Hilbert’s interpretation of quantification
Hilbert interpreted quantification in terms of his -function as follows :
“IV. The logical -axiom
Here stands for an object of which the proposition certainly holds if it holds of any object at all; let us call the logical -function.
1. By means of , “all” and “there exists” can be defined, namely, as follows:
On the basis of this definition the -axiom IV(13) yields the logical relations that hold for the universal and the existential quantifier, such as:
… (Aristotle’s dictum),
… (principle of excluded middle).”
Thus, Hilbert’s interpretation of universal quantification— defined in (i)—is that the sentence holds (under a consistent interpretation ) if, and only if, holds whenever holds for any given (in ); hence does not hold for any (since is consistent), and so holds for any given (in ).
Further, Hilbert’s interpretation of existential quantification—defined in (ii)—is that holds (in ) if, and only if, holds for some (in ).
Brouwer’s objection to such an unqualified interpretation of the existential quantifier was that, for the interpretation to be considered sound when the domain of the quantifiers under an interpretation is infinite, the decidability of the quantification under the interpretation must be constructively verifiable in some intuitively and mathematically acceptable sense of the term `constructive’ .
Two questions arise:
(a) Is Brouwer’s objection relevant today?
(b) If so, can we interpret quantification `constructively’?
The standard interpretation of PA
We consider the structure , defined as:
… the set of natural numbers;
… the successor function;
… the addition function;
… the product function;
… the null element,
that serves for a definition of today’s standard interpretation, say , of the first-order Peano Arithmetic PA.
Now, if and are PA-formulas, and the relation is the interpretation in of the PA-formula then, in current literature:
(1a) is defined true in if, and only if, for any given natural number , the sentence holds in ;
(1b) is an abbreviation of , and is defined as true in if, and only if, it is not the case that, for any given natural number , the sentence holds in ;
(1c) holds in for some natural number if, and only if, it is not the case that, for any given natural number , the sentence holds in .
Since (1a), (1b) and (1c) together interpret and in as intended by Hilbert’s -function, they attract Brouwer’s objection.
This answers question (a).
A finitary model of PA
Clearly, the specific target of Brouwer’s objection is (1c), which appeals to Platonically non-constructive, rather than intuitively constructive, plausibility.
We can thus re-phrase question (b) more specifically: Can we define an interpretation of PA over that does not appeal to (1c)?
Now, it follows from Turing’s seminal 1936 paper on computable numbers that every quantifier-free arithmetical function (or relation, when interpreted as a Boolean function) defines a Turing-machine .
We can thus define another interpretation over the structure  where:
(2a) is defined as true in if, and only if, the Turing-machine evidences  the assertion denoted by as always true (i.e., as true for any given natural number ) in ;
(2b) is an abbreviation of , and is defined as true in if, and only if, it is not the case that the Turing-machine evidences the assertion denoted by as always false (i.e., as false for any given natural number ) in .
We note that is a finitary model of PA since—when interpreted suitably —all theorems of first-order PA are constructively true in .
This answers question (b).
Are both interpretations of PA over the structure sound?
The structure can thus be used to define both the standard interpretation and a finitary model for PA.
However, in the finitary model, from the PA-provability of , we may only conclude that does not algorithmically compute as always true in .
We may not conclude further that must algorithmically compute as false in for some natural number , since may be a Halting-type of function that is not algorithmically computable .
In other words, we may not conclude from the PA-provability of that does not hold in for some natural number .
The question arises: Are both the interpretations and of PA over the structure sound?
PA is –inconsistent
Now, Gödel has shown  how to construct an arithmetical formula such that, if PA is assumed simply consistent, then is PA-provable for any given numeral , but is not PA-provable.
He further showed  it would follow that if PA is additionally assumed to be -consistent, then too is not PA-provable.
Now, Gödel also defined  a formal language as -consistent if, and only if, there is no -formula for which:
(i) is -provable,
(ii) is -provable for any given numeral of .
However, a significant consequence of the finitary proof of the consistency of PA in this paper on evidence-based interpretations of PA  is that the formula is PA-provable, and so PA is –inconsistent!
The interpretation of PA over the structure is not sound
Now, holds for any given natural number since Gödel has defined  such that is instantiationally equivalent to a primitive recursive relation which is algorithmically computable as true in for any given natural number by the Turing-machine .
It follows that we cannot admit the standard Hilbertian interpretion of in as:
is false for some natural number .
In other words, the interpretation of PA over the structure is not sound.
However, we can interpret in as:
It is not the case that the Turing-machine algorithmically computes as true in for any given natural number .
Moreover, the -inconsistent PA is consistent with the finitary interpretation of quantification in (2a) and (2b), since the interpretation of PA over the structure is sound .
Why the interpretation of PA over is not sound
The reason why the interpretation of PA over the structure is not sound lies in the fact that, whereas (1b) and (2b) preserve the logical properties of formal PA-negation under interpretation in and respectively, the further non-constructive inference in (1c) from (1b)— to the effect that must hold in for some natural number —does not, and is the one objected to by Brouwer.
If we assume only simple consistency for Hilbert’s system, then we cannot unconditionally define:
is true in if, and only if, holds for some natural number in .
This follows since, if is true in if, and only if, holds for some natural number in , then PA is necessarily -consistent — which is not the case.
Thus the interpretation is not a model of PA, and Brouwer was justified in his objection to Hilbert’s unqualified interpretation of quantification.
Br08 L. E. J. Brouwer. 1908. The Unreliability of the Logical Principles. English translation in A. Heyting, Ed. L. E. J. Brouwer: Collected Works 1: Philosophy and Foundations of Mathematics. Amsterdam: North Holland / New York: American Elsevier (1975): pp.107-111.
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.
Hi27 David Hilbert. 1927. The Foundations of Mathematics. In The Emergence of Logical Empiricism. 1996. Garland Publishing Inc.
Hi30 David Hilbert. 1930. Die Grundlegung der elementaren Zahlenlehre. Mathematische Annalen. Vol. 104 (1930), pp.485-494.
Mu91 Chetan R. Murthy. 1991. An Evaluation Semantics for Classical Proofs. Proceedings of Sixth IEEE Symposium on Logic in Computer Science, pp. 96-109, (also Cornell TR 91-1213), 1991.
Tu36 Alan Turing. 1936. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp.544-546. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. pp.116-154.
An07 Bhupinder Singh Anand. 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: Hi27, p.466.
Return to 2: Br08.
Return to 3: Tu36, pp.138-139.
Return to 4: As detailed in An12.
Return to 5: We note that we can, in principle, define the classical `satisfaction’ and `truth’ of the formulas of a first order arithmetical language such as PA constructively under an interpretation using as evidence the computations of a simple functional language (in the sense of Mu91).
Return to 6: As detailed in An12.
Return to 7: cf. Tu36, pp.132.
Return to 8: Go31, pp.25(1).
Return to 9: Go31, pp.26(2).
Return to 10: Go31, pp.23.
Return to 11: cf. An12.
Return to 12: Go31, pp.24)
Return to 13: As detailed in An12.