Is Hilbertian quantification currently interpreted constructively over infinite mathematical domains?
We consider next the first—and more significant—issue of whether the currently accepted interpretations of formal quantification—essentially as defined by David Hilbert in his formalisation of Aristotle’s logic of predicates in terms of his -function  —can be treated as constructive over an infinite domain.
Now, classical theory follows the 2000-year old philosophical perspective of Greek philosophers such as Aristotle, and asks only that the `core’ axioms of a formal language, and its rules of inference, be interpretable—under Alfred Tarski’s inductive definitions of the satisfiability and truth of the formulas of a formal language under an interpretation  —as `self-evidently’ sound  propositions.
The subjective—and essentially irresolvable—element in the `soundness’ of such a viewpoint is self-evident.
L. E. J. Brouwer  emphatically (and, as we shall show, justifiably so far as number theory was concerned) objected to such subjectivity, and asserted that Hilbert’s interpretations of formal quantification were non-constructive.
Although Hilbert’s formalisation of the quantifiers (an integral part of his formalisation of Aristotle’s logic of predicates) appeared adequate, Brouwer rejected Hilbert’s interpretations of them on the grounds that the interpretations were open to ambiguity .
However, Brouwer’s rejection of the Law of the Excluded Middle as a resolution of the objection was seen—also justifiably  —as unconvincingly rejecting a comfortable interpretation that—despite its Platonic overtones—appeared intuitively plausible to the larger body of academics that was increasingly attracted to, and influenced by, the remarkably expressive powers provided by Cantor-inspired set theories such as ZF.
Since Brouwer’s seminal work preceded that of Alan Turing, it was unable to offer his critics an alternative—and intuitively convincing—constructive definition of quantification based on the view—gaining currency today—that a simple functional language can be used for specifying evidence for propositions in a constructive logic .
Moreover, since Brouwer’s objections did not gain much currency amongst mainstream logicians, they were unable to influence Turing who, it is our contention, could easily have provided the necessary constructive interpretations  sought by Hilbert for number theory, had Turing not been influenced by Gödel’s powerful presentation—and Gödel’s persuasive Platonic interpretation of his own formal reasoning in his (Gödel’s) seminal 1931 paper on formally undecidable arithmetical propositions .
Gödel’s Platonism and -consistency
Although meriting a more complete discussion than is appropriate to the intent of this investigation, it is worth noting that the roots of of Gödel’s Platonism can be cogently argued as lying—contrary to generally held opinions—purely in an axiomatic logical, rather than philosophical, presumption.
More specifically in:
Gödel’s presumption that Peano Arithmetic is -consistent .
Reason: Gödel’s presumption is equivalent to the premise—almost universally unchallenged hitherto in mainstream literature, and excepted to largely by ultra-finitists such as Alexander Yessenin-Volpin  —that:
The standard interpretation of first-order PA may be assumed to yield a model for number theory.
Rosser’s implicit presumption
A point worth noting is that common folklore mistakenly perceives J. B. Rosser’s proof of `undecidability’ as having avoided Gödel’s explicit presumption of -consistency.
Mistakenly, because the perception is illusory.
Rosser’s proof merely replaces an explicit appeal to Gödel’s presumption by an implicit presumption that the standard interpretation of first-order PA may be assumed to yield a model for number theory.
Thus Gödel’s Platonism essentially reflects the fact (as we have detailed here) that PA is -consistent if, and only if, Aristotle’s particularisation is presumed to always hold under any interpretation of the associated logic; and that the standard interpretation of PA is a model of PA if, and only if, PA is -consistent.
In this respect, Gödel was only endorsing Hilbert’s essentially Platonic formalisation of Aristotle’s Logic of Predicates  as valid.
Be that as it may, in this 1939 paper  on ordinal-based logics (essentially his 1938 PhD dissertation), Turing applied his computational method—which he had developed in his 1936 paper  —in seeking partial completeness in interpretations of Cantor’s ordinal arithmetic (as defined in a set theory such as ZF) rather than in seeking a categorical interpretation of PA .
Turing perhaps viewed his 1936 paper as complementing and extending Gödel’s and Cantor’s reasoning.
“The well-known theorem of Gödel shows that every system of logic is in a certain sense incomplete, but at the same time it indicates means whereby from a system of logic a more complete system may be obtained. By repeating the process we get a sequence of each more complete than the preceding.
… Proceeding in this way we can associate a system of logic with any constructive ordinal. It may be asked whether a sequence of logics of this kind is complete in the sense that to any problem there corresponds an ordinal such that is solvable by means of the logic . I propose to investigate this question in a more general case, and to give some other examples of ways in which systems of logic may be associated with constructive ordinals”. 
It is our contention that Turing thus overlooked the fact that his 1936 paper actually conflicts with Gödel’s and Cantor’s interpretations of their own, formal, reasoning by admitting an objective definition of satisfaction (as we have detailed here) that yields a sound, finitary, interpretation of PA.
Specifically, whereas Gödel’s and Cantor’s reasoning implicitly presumes that satisfaction under the standard interpretation of PA can only be defined non-constructively in terms of subjectively verifiable truth , it can be cogently argued that satisfaction under both and is definable constructively in terms of objective algorithmic verifiability .
As a result, current theory continued—and continues to this day—to essentially follow Hilbert’s Platonically-influenced (hence, subjective) definitions and interpretations of the quantifiers (based on Aristotle’s logic of predicates) when defining them under the standard interpretation  of formal number theory.
Tarski’s definitions of satisfiability and truth
Now, the latter definitions and interpretations  are, in turn, founded upon Tarski’s analysis of the inductive definability of the truth of compound expressions of a symbolic language under an interpretation in terms of the satisfaction of the atomic expressions of the language under the interpretation .
Tarski defines the formal sentence P as True if and only if p—where `p’ is the proposition expressed by `P’. In other words, the sentence `Snow is white’ may be treated as a semantic truth if, and only if, it is subjectively true in all cases; and it is subjectively true in a particular case if, and only if, it expresses the subjectively verifiable fact that snow is white in that particular case.
Thus, for Tarski the commonality of the satisfaction of the atomic formulas of a language under an interpretation is axiomatic .
The road ahead
We highlight the limitations of such subjectivity here and, in the case of the `standard’ interpretation of the Peano Arithmetic PA, show how to avoid them by requiring that the `core’ axioms of PA, and its rules of inference, be interpretable as algorithmically (and, ipso facto, objectively) verifiable `sound’ propositions.
We shall next consider the issue of when, and whether, the concept of a completed infinity is consistent with the interpretation of a formal language.
BBJ03 George S. Boolos, John P. Burgess, Richard C. Jeffrey. 2003. Computability and Logic (4th ed). Cambridge University Press, Cambridge.
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.
Fe85 Richard P. Feynman. 1985. Judging Books by Their Covers in Surely You’re Joking, Mr. Feynman! (Adventures of a curious character). Norton, New York. (Extracts: Judging Books by Their Covers.)
Ff02 Solomon Feferman. 2002. Predicativity. Source: http://math.stanford.edu/~feferman/papers/predicativity.pdf.
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.
He04 Catherine Christer-Hennix. 2004. Some remarks on Finitistic Model Theory, Ultra-Intuitionism and the main problem of the Foundation of Mathematics. ILLC Seminar, 2nd April 2004, Amsterdam.
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.
Me64 Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand.
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.
Na08 Melvyn B. Nathanson. 2008. Desperately Seeking Mathematical Truth. Opinion in the August 2008 Notices of the American Mathematical Society, Vol. 55, Issue 7.
Pa95 Charles Parsons. 1995. Platonism and Mathematical Intuition in Kurt Gödel’s Thought. The Bulletin of Symbolic Logic, Volume 1, Number 1, March 1995, pp. 44-74.
Ru53 Walter Rudin. 1953. Principles of Mathematical Analysis. McGraw Hill, New York.
Sh67 Joseph R. Shoenfield. 1967. Mathematical Logic. Reprinted 2001. A. K. Peters Ltd., Massachusetts.
Ta33 Alfred Tarski. 1933. The concept of truth in the languages of the deductive sciences. In Logic, Semantics, Metamathematics, papers from 1923 to 1938 (p152-278). ed. John Corcoran. 1983. Hackett Publishing Company, Indianapolis.
Tu36 Alan Turing. 1936. On computable numbers, with an application to the Entscheidungsproblem. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from the Proceedings of the London Mathematical Society, ser. 2. vol. 42 (1936-7), pp.230-265; corrections, Ibid, vol 43 (1937) pp. 544-546.
Tu39 Alan Turing. 1939. Systems of logic based on ordinals. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York. Reprinted from the Proceedings of the London Mathematical Society, ser. 2. vol. 45 (1939), pp.161-228.
Ya93 Stephen Yablo. 1993. Paradox without self-reference. Analysis, 53(4), pp. 251-252.
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.
Return to 2: cf. Me64, p.50.
Return to 3: The word `sound’ is occasionally used informally as a synonym for `reliable’, but mostly as a technical term of mathematical logic (cf. Me64, p.51). The distinction is assumed to be obvious from the context in which it is used.
Return to 4: Br08.
Return to 5: They could not, therefore, be accepted as admitting effective communication.
Return to 6: Reason: Although Hilbert’s formalisation and interpretation of the quantifiers implies that the Law of the Excluded Middle must hold in any model of the formalisation, the converse is not true.
Return to 7: Mu91.
Return to 8: Detailed in An12.
Return to 9: Go31.
Return to 10: Go31, p.28.
Return to 11: Pa95, Ff02
Return to 12: In Go31.
Return to 13: As outlined in He04.
Return to 14: Hi27, p.466.
Return to 15: Tu39.
Return to 16: Tu36.
Return to 17: Perhaps since such a search would involve questioning either the validity of Gödel’s belief that systems of Arithmetic such as PA are -consistent, or Gödel’s interpretation of his 1931 `undecidability’ argument as having meta-mathematically proven that systems of Arithmetic such as PA are essentially incomplete!
Return to 18: Tu39, pp.155-156
Return to 19: A view (such as here) reflected in the not uncommon interpretation of Tarski’s Theorem (see Me64, p.151) as establishing the formal undefinability of arithmetical truth in arithmetic. We shall show why such an interpretation is untenable.
Return to 21: cf. Me64, p.107; Sh67, p.23, p.209; BBJ03, p.104. For purposes of this investigation, we treat Me64 as a reliable and representative exposition—where cited—of the standard logical concepts and theory that are addressed at that point.
Return to 22: eg. Me64, pp.49-53.
Return to 23: Ta33.
Return to 24: cf. Me64, p.51(i).