On 5 Mar 2008, at 09:11, Vaughan Pratt wrote: VP>> My feeling about ... Brouwerian modes of thoughts is that they are ... great stories about things that never actually happened ... I happen to find Excluded Middle more convenient than its negation, but that's just me and perhaps others have had the opposite experience. <<VP I suspect that this feeling is shared to a greater or lesser degree by most practicing mathematicians. I also suspect that it arises out of perceptions based on Brouwer's interpretation and subsequent assessment of his own, original, objection to Hilbert's particular expression of The Law of the Excluded Middle, rather than on a perception of what it was that Brouwer was actually objecting to and rejecting. In other words, such perceptions may be vulnerable to the "cover-up" syndrome remarked upon by Physicist Richard P. Feynman in his 1965 Nobel Lecture: We have a habit in writing articles published in scientific journals to make the work as finished as possible, to cover up all the tracks, to not worry about the blind alleys or describe how you had the wrong idea first, and so on. So there isnt any place to publish, in a dignified manner, what you actually did in order to get to do the work. I believe that Brouwer's "finished" articulation of his objection to Hilbert's position vis-à-vis the foundations of logical reasoning may be an instance of such unconscious cover up; if so, it is one that has had an unintended, far-reaching and severely limiting consequences on a discipline. The basis for my belief lies in Hilbert's interpretation of the universal and existential quantifiers, which is detailed, for instance, in his 1927 paper "The Foundations of Mathematics". In this paper, Hilbert defines the quantifiers in terms of his epsilon-function as: (i) The formal sentence [(All x)F(x)] holds under a consistent interpretation I if, and only if, the interpreted relation F(s) holds whenever ~F(s) holds for any given s in I; hence ~F(s) does not hold for any s in I (since I is consistent}), and so F(s) holds for any given s in I. (ii) The formal sentence [(Exists x)F(x)] holds in I if, and only if, the interpreted relation F(s) holds for some s in I. He then deduces from it "Aristotle's dictum" and the "principle of the excluded middle": (iii) Aristotle's dictum: If the formal sentence [(All x)F(x)] holds in I, then the interpreted relation F(s) holds for any s in I, and: (iv) Principle of excluded middle: If the formal sentence [~(All x)F(x)] holds in I, then the formal sentence [(Exists a)(~A(a)] holds in I. (I assume that the above paper also reflects Hilbert's thesis prior to Brouwer's objection.) Now, in his 1908 paper "The Unreliability of the Logical Principles", Brouwer stressed that, for Hilbert's above 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". I doubt whether any practicing mathematician would take serious issue with this objection. I feel it is the perception that Brouwer's - and the Intuitionistic - objection relates specifically to the Law of the Excluded Middle - of which (iv) is merely one statement - that seems to give rise to the sense of disquietitude expressed by Vaughan Pratt in his above cited post. The reasons for such disquietitude are not far to seek. Currently it is implicitly accepted (as intuitively plausible) by practicing mathematicians that, in first-order Peano Arithmetic (PA) for instance: (1) The PA-formula [(Exists x)F(x)] is an abbreviation of [~(All x)~F(x)], and is defined as true in the standard interpretation M of PA if, and only if, it is not the case that, for any given natural number n, the interpreted relation ~F(n) holds in M; (2) The interpreted relation F(n) holds in M for some natural number n if, and only if, it is not the case that, for any given natural number n, ~F(n) holds in M. Now, since (1) and (2) together interpret (Exists x)F(x) in M as intended by Hilbert's epsilon-function, they similarly attract Brouwer's objection - which, thus, remains unresolved in current literature. Thus, for a practicing mathematician today, the Intuitionistic rejection of the Law of the Excluded Middle should be tantamount to rejecting the standard interpretation of first-order PA as a valid model for PA. This is not obvious if Brouwer's objection is perceived as primarily rejecting Hilbert's principle of the excluded middle (iv), since the latter may have other avatars, not all of which need attract Brouwer's objection. In other words, Brouwer's objection needs to be seen not as rejecting the Law of the Excluded Middle per se, but as specifically rejecting only Hilbert's interpretation of the existential quantifier in (ii). The point to note then is that, whereas (1) by itself preserves the formal properties of PA-negation under interpretation in M, the further inference in (2) from (1) does not; and it is this inference that is objected to by Brouwer. Moreover, Brouwer's objection becomes significant only if we accept that (2) appeals to Platonically non-constructive, rather than intuitively constructive, plausibility. Since most practicing mathematicians are comfortable with informal Platonic reasoning, but uncomfortable with formal reasoning that cannot be interpreted constructively, it is this aspect of (2) that appears to place them on the horns of the following dilemma: Even if we accept that the existential quantifier is interpreted non-constructively in current literature by accepting (2), how do we interpret such quantification constructively without sacrificing mathematical reasoning and mathematical structures that a practicing mathematician intuitively accepts as well-founded? This is the grey area that Intuitionistic - and finitist - reasoning have sought to address since Brouwer, primarily by focusing on what remains of classical mathematics (post Hilbert) after rejecting (2) above. The problem, of course, is that rejection of a widely - even if uncomfortably - held tenet is never a solution unless one replaces it with one that is less uncomfortable. This is the "It's better to live in a house with a leaking roof, than to bring the roof down over one's head" syndrome. So the question is: Can we provide a "comfortable", finitary, interpretation of PA that accepts (1), but rejects (2) if necessary? I believe that every practicing mathematician knows that the answer to this question must be a "yes', since mathematical languages seem to communicate effectively in practice in all areas of human endeavour. In other words, every practicing mathematician knows that the significant body of mathematical reasoning and structures is founded on a finitary foundation. The issue, therefore, is simply one of identifying the structure. Now Turing has shown in his seminal 1936 paper on computable numbers that every arithmetical function (or relation, when interpreted as a Boolean function) F defines a Turing-machine TM_F. This suggests the possibility of replacing (1) by: (3) The PA-formula [(Exists x)F(x)] is an abbreviation of [~(All x)~F(x)], and is defined as true in an interpretation B of PA if, and only if, it is not the case that the Turing-machine TM_F computes F(n) as always false (i.e., as false for any given natural number n in B). Now, I have shown in the Dec07 issue of the on-line journal, The Reasoner, that an interpretation along these lines is actually a finitary model for PA, since all theorems of PA interpret as true in B. http://www.thereasoner.org/ Moreover, the interpretation B satisfies Brouwer's criteria, since - by virtue of Turing's Halting argument - the mirror of (2) does not hold in B. In other words, in the finitary model B, from the PA-provability of [~(All x)F(x)], we may only conclude that TM_F does not compute F(n) as always true in B. We may not conclude further that TM_F must compute F(n) as false in B for some natural number n, since F(x) may be a Halting-type of function that is not Turing-computable. What this means is that we may not conclude from the PA-provability of [~(All x)F(x)] that F(n) does not hold in B for some natural number n. Of course the consequences of such a finitary model for PA are far-reaching, since it (expectedly?) follows that the accepted standard (non-constructive) interpretation of PA - which is based on accepting (2) above - is not a model of PA! I address the above points in detail in a series of commentaries in the Sep07, Oct07, Nov07, Dec07 and Jan08 issues of The Reasoner and in two papers that I am compiling for publication: * Why Brouwer was justified in his objection to Hilbert's unqualified interpretation of quantification http://alixcomsi.com/9_Why_Brouwer_was_justified_Rev_1000.pdf * Is PvNP formulated adequately? http://alixcomsi.com/Is_PvNP_formulated_adequately_Update.pdf Sincerely, Bhup