Principia Mathematica is modern and insightful

The above proposition gives what is in practice the only way of proving existence theorems: we always have to find some particular y for which φy holds, and hence to infer (∃x).φx. If we were to assume what is called the multiplicative axiom, or the equivalent axiom enunciated by Zermello, that would, in an important class of cases, give an existence-theorem where no particular instance of truth can be found. Jacques Carette noted that Brouwer was also publishing around that time. (Although it has to be said that Brouwer writings of that time were hardly comprehensible to a mathematician. The intuitionistic vs. classical controversy has really started with Hermann Weyl.) Jacques has further noted that some aspects of that constructivism can be traced back Kronecker 30 years earlier. Types ⊢ ∀x. φ(x) ∧ ∀x. ψ(x) ⇒ ∀x. φ(x) ∧ ψ(x) Origin of set-membership Descriptive functions Principia calls such binary-relation--induced functions `descriptive functions' (now often called ``definite descriptions'). The name and the exposition follows the theory of descriptions in natural languages that Russell developed five years prior (in his famous paper ``On denoting'', Mind 14(4), 1905). Jacques Carette noted that Principia anticipated the difference between ``definite description'' and ``explicit function'' back in 1910, because there were already examples in mathematics of these. ``Analytic continuation is one of those processes in mathematics which is functional but not a function, as it involves a certain amount of choice.'' References Ludlow, Peter. Descriptions The Stanford Encyclopedia of Philosophy (Winter 2023 Edition), Edward N. Zalta & Uri Nodelman (eds.)