Hilbert’s formalisation of Aristotle’s logic of predicates
A fundamental tenet of classical logic—unrestrictedly adopted by formal first-order predicate calculus as axiomatic —is Aristotlean particularisation.
Aristotlean particularisation: This holds that an assertion such as:
`There exists an unspecified such that holds’
—usually denoted symbolically by `‘—can always be validly inferred in the classical, Aristotlean, logic of predicates  from the assertion:
`It is not the case that: for any given , does not hold’
—usually denoted symbolically by `‘.
In a 1927 address, Hilbert reviewed, as part of his `proof theory’, his axiomatisation of classical Aristotle’s logic of predicates as a formal first-order -predicate calculus .
A specific aim of the axiomatisation appears to have been the introduction of a primitive choice-function symbol, `‘, for formalising the existence of the unspecified object in Aristotle’s particularisation :
“… stands for an object of which the proposition certainly holds if it holds of any object at all …” 
“… The fundamental idea of my proof theory is none other than than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds.”
More precisely :
Lemma adequately expresses—and yields, under a suitable interpretation—Aristotle’s logic of predicates if the -function is interpreted so as to yield the unspecified object in Aristotlean particularisation.
What came to be known later as Hilbert’s Program  —which was built upon Hilbert’s `proof theory’—can be viewed as, essentially, the subsequent attempt to show that the formalisation was also necessary for communicating Aristotle’s logic of predicates effectively and unambiguously under any interpretation of the formalisation.
This goal is implicit in Hilbert’s remarks :
“Mathematics in a certain sense develops into a tribunal of arbitration, a supreme court that will decide questions of principle—and on such a concrete basis that universal agreement must be attainable and all assertions can be verified.”
“… a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument.”
The postulation of an `unspecified’ object in Aristotle’s particularisation is `stronger’ than the Axiom of Choice
The difficulty in attaining this goal constructively along the lines desired by Hilbert—in the sense of the above quotes—becomes evident from Rudolf Carnap’s analysis in a 1962 paper, “On the use of Hilbert’s -operator in scientific theories” .
Carnap noted that if we define a formal language ZF by replacing:
in the Zermelo-Fraenkel set theory ZF, then:
Lemma The Axiom of Choice is a theorem of ZF, and therefore true in any sound interpretation of the Zermelo-Fraenkel set theory ZF that admits Aristotle’s logic of predicates.
Thus, the postulation of an `unspecified’ object in Aristotlean particularisation is a stronger postulation than the Axiom of Choice!
Cohen and The Axiom of Choice
The significance of this is seen in the accepted interpretation of Cohen’s argument in his 1963-64 papers ; the argument is accepted as definitively establishing that the Axiom of Choice is essentially independent of a set theory such as ZF.
Now, Cohen’s argument—in common with the arguments of many important theorems in standard texts on the foundations of mathematics and logic—appeals to the unspecified object in Aristotle’s particularisation when interpreting the existential axioms of ZF (or statements about ZF ordinals).
(Downwards) Löwenheim-Skolem Theorem : If a first-order proposition is satisfied in any domain at all, then it is already satisfied in a denumerably infinite domain.
Now, the significance of Hilbert’s formalisation of Aristotle’s particularisation by means of the -function is seen in Cohen’s following remarks, where he explicitly appeals in the above argument to a semantic—rather than formal—definition of the unspecified object in Aristotle’s particularisation :
“When we try to construct a model for a collection of sentences, each time we encounter a statement of the form we must invent a symbol and adjoin the statement . … when faced with , we should choose to have it false, unless we have already invented a symbol for which we have strong reason to insist that be true.”
Cohen, then, shows that the the Axiom of Choice is false in N.
Any interpretation of ZF which appeals to Aristotle’s particularisation is not sound
Since Hilbert’s -function formalises precisely Cohen’s concept of `‘—more properly, `‘—as , it follows that:
Theorem If the underlying logic is classical first order logic in which the quantifiers are interpreted according to Aristotle’s logic of predicates, then any model of ZF is a model of ZF plus the logical -axiom, since the expression must interpret to yield Cohen’s symbol `‘ whenever interprets as true.
(Note that we cannot argue that ZF is a conservative extension of ZF.)
Hence Cohen’s argument is also applicable to ZF plus the logical -axiom.
However, since the Axiom of Choice is true in any sound interpretation of ZF plus the logical -axiom which appeals to Aristotle’s logic of predicates, Cohen’s argument  —when applied to ZF plus the logical -axiom—actually shows that:
Corollary ZF plus the logical -axiom has no model that appeals to Aristotle’s logic of predicates.
Corollary ZF has no model that appeals to Aristotle’s particularisation.
We cannot, therefore, conclude that the Axiom of Choice is essentially independent of the axioms of ZF, since none of the putative models `forced’ by Cohen (in his argument for such independence) are defined by a sound interpretation of ZF.
Cohen and the Gödelian Argument
At the conclusion of his lectures on “Set Theory and the Continuum Hypothesis”, delivered at Harvard University in the spring term of 1965, Cohen remarked :
“We close with the observation that the problem of CH is not one which can be avoided by not going up in type to sets of real numbers. A similar undecidable problem can be stated using only the real numbers. Namely, consider the statement that every real number is constructible by a countable ordinal. Instead of speaking of countable ordinals we can speak of suitable subsets of . The construction for , where is countable, can be completely described if one merely gives all pairs such that . This in turn can be coded as a real number if one enumerates the ordinals. In this way one only speaks about real numbers and yet has an undecidable statement in ZF. One cannot push this farther and express any of the set-theoretic questions that we have treated as statements about integers alone. Indeed one can postulate as a rather vague article of faith that any statement in arithmetic is decidable in “normal” set theory, i.e., by some recognizable axiom of infinity. This is of course the case with the undecidable statements of Gödel’s theorem which are immediately decidable in higher systems.”
Cohen appears to assert here that if ZF is consistent, then we can `see’ that the Continuum Hypothesis is subjectively true for the integers under some model of ZF, but—along with the Generalised Continuum Hypothesis—we cannot objectively `assert’ it to be true for the integers since it is not provable in ZF, and hence not true in all models of ZF.
However, by this argument, Gödel’s undecidable arithmetical propositions, too, can be `seen’ to be subjectively true for the integers in the standard model of PA, but cannot be `asserted’ to be true for the integers since the statements are not provable in an -consistent PA, and hence they are not true in all models of an -consistent PA!
As I have argued in The Reasoner , the argument is plausible, but unsound. It is based on a misinterpretation—of what Gödel actually proved formally in his 1931 paper—for which, moreover, neither Lucas nor Penrose ought to be taken to account.
The distinction sought to be drawn by Cohen is curious, since we have shown that his argument—which assumes that sound interpretations of ZF can appeal to Aristotle’s particularisation—actually establishes that sound interpretations of ZF cannot appeal to Aristotle’s particularisation; just as we shall show that Gödel’s argument  actually establishes that any sound interpretation of PA, too, cannot appeal to Aristotle’s particularisation.
Loosely speaking, the cause of the undecidability of the Continuum Hypothsis—and of the Axiom of Choice—in ZF as shown by Cohen, and that of Gödel’s undecidable proposition in Peano Arithmetic, is common; it is interpretation of the existential quantifier under an interpretation as Aristotlean particularisation.
In Gödel’s case it is made explicitly—but formally to avoid attracting intuitionistic objections—through his specification of what he believed to be a `much weaker assumption’  of -consistency for his formal system P of Peano Arithmetic .
Ca62 Rudolf Carnap. 1962. On the use of Hilbert’s -operator in scientific theories. In Essays on the Foundations of Mathematics. Edited by Y. Bar-Hillel, E. I. J. Posnanski, M. O. Rabin, and A. Robinson for The Hebrew University of Jerusalem. 1962. North Holland Publishing Company, Amsterdam: pp.156-164.
Co63 Paul J. Cohen. The Independence of the Continuum Hypothesis I. Proceedings of the U. S. National Academy of Sciences. 50, 1143-1148, 1963.
Co64 Paul J. Cohen. The Independence of the Continuum Hypothesis II. Proceedings of the National Academy of Sciences of the United States of America, 51(1), 105 110, 1964.
Co66 Paul J. Cohen. 1966. Set Theory and the Continuum Hypothesis. (Lecture notes given at Harvard University, Spring 1965) W. A. Benjamin, Inc., New York.
Go31 Kurt Gödel. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Elliott Mendelson. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. pp.5-38.
HA28 David Hilbert & Wilhelm Ackermann. 1928. Principles of Mathematical Logic. Translation of the second edition of the Grundzüge Der Theoretischen Logik. 1928. Springer, Berlin. 1950. Chelsea Publishing Company, New York.
Hi25 David Hilbert. 1925. On the Infinite. Text of an address delivered in Münster on 4th June 1925 at a meeting of the Westphalian Mathematical Society. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.
Hi27 David Hilbert. 1927. The Foundations of Mathematics. Text of an address delivered in July 1927 at the Hamburg Mathematical Seminar. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.
Lo15 Leopold Löwenheim. 1915. On possibilities in the calculus of relatives. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.
Lu61 J. R. Lucas. 1961. Minds, Machines and Gödel. Philosophy, XXXVI, 1961, pp.112-127; reprinted in The Modeling of Mind. Kenneth M. Sayre and Frederick J. Crosson, eds., Notre Dame Press, 1963, pp.269-270; and Minds and Machines, ed. Alan Ross Anderson, Prentice-Hall, 1954, pp.43-59.
Pe90 Roger Penrose. 1990. The Emperor’s New Mind: Concerning Computers, Minds and the Laws of Physics. 1990, Vintage edition. Oxford University Press.
Pe94 Roger Penrose. 1994. Shadows of the Mind: A Search for the Missing Science of Consciousness. Oxford University Press.
Sh67 Joseph R.\ Shoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.
Sk22 Thoralf Skolem. 1922. Some remarks on axiomatized set theory. Text of an address delivered in Helsinki before the Fifth Congress of Scandinavian Mathematicians, 4-7 August 1922. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.
Sk28 Thoralf Skolem. 1928. On Mathematical Logic. Text of a lecture delivered on 22nd October 1928 before the Norwegian Mathematical Association. In Jean van Heijenoort. 1967. Ed. From Frege to Gödel: A source book in Mathematical Logic, 1878 – 1931. Harvard University Press, Cambridge, Massachusetts.
Wa63 Hao Wang. 1963. A survey of Mathematical Logic. North Holland Publishing Company, Amsterdam.
An07a Bhupinder Singh Anand. 2007. The Mechanist’s Challege. The Reasoner, Vol(1)5 p5-6.
An07 … 2007. Why we shouldn’t fault Lucas and Penrose for continuing to believe in the Gödelian argument against computationalism – I. The Reasoner, Vol(1)6 p3-4.
An12 Bhupinder Singh Anand. 2012. Evidence-Based Interpretations of PA. In Proceedings of the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012, 2-6 July 2012, University of Birmingham, Birmingham, UK.
Return to 1: See Hi25, p.382; HA28, p.48; Sk28, p.515; Be59, pp.178 & 218; Co66, p.4.
Return to 2: HA28, pp.58-59.
Return to 3: Hi27, pp.465-466.
Return to 5: Note that need not be a `term’ of , since it is a term if, and only if, `holds’ for some term .
Return to 6: Hi27, p.475.
Return to 7: cf. Hi25, pp.382-383; Hi27, p.466(1).
Return to 9: Hi25, p.384; Hi27, p.475. Eighty years down the line, Hilbert’s optimistic vision of `a tribunal of arbitration’ stands in stark contrast to the `tribunal of bosses’ reflected in Melvyn B. Nathanson’s despairing comments here!
Return to 10: Ca62, pp.157-158; see also Wang’s remarks in Wa63, pp.320-321.
Return to 11: Co63 & Co64.
Return to 12: Co66, p.19.
Return to 13: See Skolem’s remarks in Sk22, p295; also Co66, p.19.
Return to 14: Lo15, p.245, Theorem 6; Sk22, p.293.
Return to 15: Co66, p.19 & p.82.
Return to 16: Co66, p.121.
Return to 17: Co66, p.83 & p.112-118.
Return to 18: Co66, p.112; see also p.4.
Return to 19: Co63 & Co64; Co66.
Return to 20: Co66, p.151.
Return to 21: Lu61.
Return to 22: Pe94.
Return to 23: Pe90.
Return to 24: An07a; An07b; An07c.
Return to 28: Go31, p.24, Theorem VI.
Return to 29: Co66, p.4.
Return to 30: Co66 p.112.}
Return to 31: The significance of Gödel’s `much weaker assumption’ is highlighted in An12, where we note that, a Peano Arithmetic has a sound interpretation that appeals to Aristotle’s particularisation—such as the interpretation currently defined as the `standard’ interpretation of the first order Peano Arithmetic PA—if, and only if, the Arithmetic is -consistent.
Return to 32: Go31, p.9 & pp.23-24.