by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Mathematics, Calculus, Geometry, Entry Directory]
[Logic and Semantics, entry directory]
[Walter P. van Stigt, entry directory]
[Paolo Mancosu, entry directory]
[Mancosu & van Stigt, “Intuitionistic Logic,” entry directory]
[The following is summary. I am not a mathematician, so please consult the original text instead of trusting my summarizations. Bracketed comments are my own. Proofreading is incomplete, so please forgive my mistakes.]
Summary of
Paolo Mancosu & Walter P. van Stigt
“Intuitionistic Logic”
in
From Brouwer to Hilbert:
The Debate on the Foundations of Mathematics in the 1920’s
Part IV
“Intuitionistic Logic”
Part IV’s Introduction:
“Intuitionistic Logic”
4.2
The Emergence of the Intuitionistic Propositional Calculus
Brief summary:
(4.2.1) Brouwer says that the intuitionist mathematician rejects excluded middle and double negation but accepts A → ¬¬A (so if something is proven, it cannot be disproven), (A → B) → (¬B → ¬A), and ¬A is equivalent to ¬¬¬A, meaning that “one can always strike out an even number of negations from a formula provided the last negation is not cancelled” (277). (4.2.2) After Brower’s reflections on intuitionistic logic in 1923, the next to have reflected on it was Wavre in 1926. He calls classical logic “formal logic” and intuitionistic logic “empiricist” logic. He says that in an empiricist context, to assert a statement A means to assert the provability of A. And the negation of A would be stating that the assertion of A leads to a contradiction. The following are other empiricist principles:
1. (A → B) & (B → C) → (A → C);
2. From A and (A → B) one can infer B;
3. ¬(A & ¬A);
4. (A → ⊥) → ¬A.
And as with intuitionism, empiricist logic does not have excluded middle or double negation. Also valid are A → ¬¬A and the equivalence of ¬A and ¬¬¬A. Only some forms of reductio ad absurdum hold in empiricist logic. (4.2.3) Although Wavre’s article does not go beyond Brouwer’s remarks on Intuitionistic logic, it did start a debate on intuitionistic mathematics in the Revue de Metaphysique et de Morale. (4.2.4) In his 1927 book Mathematische Existenz, O. Becker gives a phenomenological interpretation of intuitionistic logic based on Husserl’s theory of judgments in his Logic Investigations. We consider that “p holds,” written as “+p”. Becker says that there are two ways this can be denied: {1} we can say p’s negation holds, “¬p holds”, written as “+(–p),” or {2} we can say p fails to hold, “p does not hold”, written as and “– (+p)”. “He also claimed that the three cases excluded any other possibility so that either +p or +(–p) or –(+p), quartum non datur.” These correspond to the ways an intention can be fulfilled. Suppose that we have the proposition p: “the book is on the table”. {1} Fulfillment [Erfüllung], +p, would be that we perceive the table and see that the book is in fact on it; {2} frustration [Enttäuschung], +(–p), would be that we see the table and the book is not on it. In this case, there would be a conflict [Widerstreit]; and {3} nonfulfillment, –(+p), would be that we see neither the table nor the book. In this case, there is no conflict. (4.2.5) Becker defines truth and falsity in intuitionistic logic in the following way: “intuitionistic logic does not distinguish between ‘true’ and ‘false’ but between ‘true’ and ‘absurd.’ In this context ‘true’ means: actually provable (constructively), and absurd: ‘provably contradictory’ (from the phenomenological point of view one can in principle say: true = there is the synthesis of the fulfillment of the judgment intention, the agreement between what is intended and what is perceived; ‘absurd’: = there is the ‘synthesis’ of the frustration of the judgment intention, the ‘synthesis’ of the conflict.... Clearly there is no complete disjunction, in the sense of the tertium non datur, between fulfillment and frustration, agreement and conflict. (Becker 1927, p. 775)” (278). (Now take the book and table example again. Suppose we do not see that the book is on the table, that is, –(+p). Now suppose instead that we do not see that the book is not on the table, or –(–p). What, phenomenologically speaking, is the difference? There is no difference between the experiences of failing to see that the book is on the table compared with failing to see that the book is not on the table. Becker found this problematic, because the quartum non datur is +p or +(–p) or –(+p) and Wavre says that in intuitionistic logic we cannot have (p ∨ ¬p ∨ ¬¬p), but here Becker thinks that we should have the equivalent of ¬¬p as –(–p).) His solution for this was not satisfactory. (4.2.6) “Becker managed to ground all the principles in Wavre’s list according to his phenomenological interpretation. At the end of the appendix he also stated the problem of finding a calculus for intuitionistic logic” (279). (4.2.7) Regarding the formulation of a calculus for intuitionistic logic, early on there were detractors. In 1927, Barzin and Errera argued that intuitionistic logic has a third value, “tierce,” written as “p′” and that on account of it and the semantics of intuitionism, the system leads to formal contradictions regarding the truth values. But their proofs involve using principles that are classically valid but not intuitionistically valid, so their attempt fails. (4.2.8) In 1928, Church, in his “On the Law of the Excluded Middle”, reviews Barzin & Errera’s criticisms and makes the following three claims: {1} Dropping the law of excluded middle alone will not result in contradictions. {2} Barzin & Errera’s criticisms use reductio ad absurdum argumentation. But reductio arguments use the law of excluded middle, so these criticisms will not work for intuitionists who reject that law. And {3} Church incorrectly says that the “tierce” value being neither true nor false breaks the law of contradiction along with the law of excluded middle. (4.2.9) Church did not see any reason for accepting the quartum non datur. (4.2.10) Glivenko in a 1928 paper shows that Brouwerian intuitionistic logic is not a three-valued logic, so the use of “tierce” propositions are invalid. (4.2.11) Glivenko in a 1929 paper provides “the first seeds of a development that will yield a long series of interpretations of classical logic into intuitionistic logic known as double negation interpretations or negative translations” (280-281). (4.2.12) Around the same time, Heyting was formalizing the principles of intuitionistic logic. (4.2.13) In a letter to Becker from 1933, Heyting explains some of his insights into intuitionistic logic and how he came upon them. (4.2.14) In other papers Heyting gives the interpretations for logical connectives in intuitionistic logic. There we also see elements of Becker’s phenomenological interpretation. (4.2.15) Heyting also says that we cannot simply identify “ ‘p is true’ (in the intuitionistic sense) with ‘p is provable’,” because we need “the observation of an empirical fact, that is, of the realization of the expectation expressed by the proposition p. Here, then, is the Brouwerian assertion of p: It is known how to prove p. (1930a, p. 307)” (282). (4.2.16) For Heyting and Kolmogorov, a proposition p can be interpreted either as an expectation or a problem. (4.2.17) Kolmogorov in 1932 explains the problem interpretation: “If a and b are two problems, then a & b designates the problem ‘to solve both problems a and b,’ while a ∨ b designates the problem ‘to solve at least one of the problems a and b.’ Furthermore, a ⊃ b is the problem ‘to solve b provided that the solution for a is given’ or, equivalently, ‘to reduce the solution of b to the solution of a’ [ ... ] ¬a designates the problem ‘to obtain a contradiction provided that the solution of a is given.’ (1932, p. 329)” (282). (4.2.18) We have thus seen three major events in the history of intuitionistic logic: “Heyting had provided a complete formalization of intuitionistic logic, Glivenko had pointed the way to the negative interpretations to follow, and the combined work of Heyting and Kolmogorov had given an explicit formulation to what is now known as the BHK interpretation of intuitionistic logic” (283).
[Important Valid and Invalid Formulas in Intuitionistic Logic from Brouwer]
[Wavre’s “Empiricist” (Intuitionistic) Logic]
[Wavre’s Contribution to the Debate]
[Becker’s Phenomenological Interpretation of Intuitionistic Logic]
[Truth and Falsity in Intuitionistic Logic, According to Becker]
[Becker and Intuitionistic Logic Calculus]
[Barzin & Errera’s “Tierce” Value and Their Failure to Critique Intuitionistic Logic ]
[Church’s Response to Barzin & Errera]
[Church Against Quartum non datur]
[Glivenko’s Showing Intuitionistic Logic is Not Three-Valued]
[Glivenko and Interpreting Classical into Intuitionistic Logic]
[Heyting and the Formalization of Intuitionistic Logic]
[Heyting’s Elaborations on His Insights]
[Heyting’s Account of the Logical Connectives and His Use of Becker’s Phenomenological Interpretation of Intuitionistic Logic]
[Other Features of Heyting’s Formalization]
[Heyting and Kolmogorov on Expectation and Problem]
[Kolmogorov and the Problem Interpretation]
[Summation]
Summary
[Important Valid and Invalid Formulas in Intuitionistic Logic from Brouwer]
[Brouwer says that the intuitionist mathematician rejects excluded middle and double negation but accepts A → ¬¬A (so if something is proven, it cannot be disproven), (A → B) → (¬B → ¬A), and ¬A is equivalent to ¬¬¬A, meaning that “one can always strike out an even number of negations from a formula provided the last negation is not cancelled” (277).]
[ditto]
We have seen that in 1923 Brouwer explicitly formulated a number of principles whose validity could not be accepted by the intuitionist mathematician. In particular the excluded middle and the principle of double negation were singled out as especially problematic. By contrast, Brouwer remarked that the intuitionist accepts the following principles: A → ¬¬A and (A → B) → (¬B → ¬A).1 From these two principles and the rule of modus ponens, implicitly accepted as valid, Brouwer was able to show that ¬¬¬A → ¬A and that ¬A → ¬¬¬A, that is, ¬A is equivalent to ¬¬¬A. From this it follows that in general one can always strike out an even number of negations from a formula provided the last negation is not cancelled.
(277)
1. In the following introduction we do not make a syntactic distinction between Intuitionistic and classical connectives. I will use &, ¬, →, and ∨. Moreover, Brouwer does not use any symbolism in this connection.
(283)
[Wavre’s “Empiricist” (Intuitionistic) Logic]
[After Brower’s reflections on intuitionistic logic in 1923, the next to have reflected on it was Wavre in 1926. He calls classical logic “formal logic” and intuitionistic logic “empiricist” logic. He says that in an empiricist context, to assert a statement A means to assert the provability of A. And the negation of A would be stating that the assertion of A leads to a contradiction. The following are other empiricist principles:
1. (A → B) & (B → C) → (A → C);
2. From A and (A → B) one can infer B;
3. ¬(A & ¬A);
4. (A → ⊥) → ¬A.
And as with intuitionism, empiricist logic does not have excluded middle or double negation. Also valid are A → ¬¬A and the equivalence of ¬A and ¬¬¬A. Only some forms of reductio ad absurdum hold in empiricist logic.]
[ditto]
The first interesting reflections after Brouwer 1923 concerning the principles of intuitionistic logic are found in an article by Wavre published in 1926a.2 Wavre’s article was devoted to a comparison of classical logic with the principles accepted by the intuitionist or, in his terminology, of the “logique formelle” and the “logique empiriste.”3 Wavre interprets the assertion of a statement A in an empirist context as asserting the provability of A. The negation of A is seen as stating that the assertion of A leads to a contradiction.4 Wavre proceeds to enumerate the similarities and dissimilarities between formal and empiricist logic. Similar principles:
1. (A → B) & (B → C) → (A → C);2. From A and (A → B) one can infer B;
3. ¬(A & ¬A);
4. (A → ⊥) → ¬A.
Among the different principles we find, as in Brouwer, the principle of the excluded middle and the principle of double negation. Wavre remarks that only A→ ¬¬A has an equivalent in empirical logic. Having listed these principles, he then goes on to show Brouwer’s theorem on the equivalence of ¬A and ¬¬¬A and to show that only some forms of reductio ad absurdum can be preserved in empiricist logic.
(277)
2. I am ignoring here Kolmogorov 1925, which remained largely unknown until later. Kolmogorov’s 1925 will not be analyzed in this introduction. See Wang 1967.
3. The use of the word empirist in this context goes back to the characterization of Du Bois-Reymond.
4. “Distinguons la logique formelle, logique de la négation ou encore du vrai et du faux, dans laquelle l’alternative s’impose entre le vrai et le faux, et la logique mathématique empiriste du vrai et de l’absurde, dans laquelle l’alternative entre le vrai et l’absurde ne s’imposerait plus; vrai signifiant l’effectivement démontrable et absurde, ce qui peut être effectivement réduit à une contradiction, la contradiction étant prise dans le sens formel” (Wavre 1926, p. 69).
(283)
Kolmogorov, A. N., 1925, O principe tertium non datur, Matematiceskij Sbornik 32, pp. 646-67. English translation in J. van Heijenoort, ed., From Frege to Gödel, Harvard University Press, Cambridge (Mass.), 1967, pp. 416-37.
(284)
Wang, H., 1967, Introductory Note to Kolmogorov 1925, in J. van Heijenoort, ed., From Frege to Gödel, Harvard University Press, Cambridge (Mass.), 1967, pp. 414-16.
Wavre, R., 1926a, Logique formelle et logique empiriste, Revue de Metaphysique et de Morale 33, pp. 65-75.
(285)
[Wavre’s Contribution to the Debate]
[Although Wavre’s article does not go beyond Brouwer’s remarks on Intuitionistic logic, it did start a debate on intuitionistic mathematics in the Revue de Metaphysique et de Morale.]
[ditto]
Although Wavre’s article does not push the analysis of intuitionistic logic much further than Brouwer’s remarks in 1923, it had, however, the merit of starting a discussion in the pages of the Revue de Metaphysique et de Morale on the nature of intuitionistic mathematics. In particular Wavre’s defense of the intuitionistic claims brought about the impatient reply of Paul Levy, who defended a more platonistic conception of mathematics (see Wavre 1924, 1926a, 1926b, Levy 1926a, 1926b, and Borel 1927). The contribution by Borel is included, as a sample of this debate, in this book.
(277)
Levy, P., 1926a, Sur le principe du tiers exclu et sur les théorèmes non-susceptibles des démonstration, Revue de Métaphysique et de Morale 33, pp. 253-58.
Levy, P., 1926b, Critique de la logique empirique, Réponse à M. Robin Wavre, Revue de Métaphysique et de Morale 33, pp. 545-51.
Wavre, R., 1924, Y-a-t-il une crise des mathematiques? A propos de la notion d’existence et d’ une application suspecte du principe du tiers exclu, Revue de Métaphysique et de Morale 31, pp. 435-70.
Wavre, R., 1926a, Logique formelle et logique empiriste, Revue de Metaphysique et de Morale 33, pp. 65-75.
Wavre, R., 1926b, Sur le principe du tiers exclu, Revue de Metaphysique et de Morale 33, pp. 425-30.
(285)
[Becker’s Phenomenological Interpretation of Intuitionistic Logic]
[In his 1927 book Mathematische Existenz, O. Becker gives a phenomenological interpretation of intuitionistic logic based on Husserl’s theory of judgments in his Logic Investigations. We consider that “p holds,” written as “+p”. Becker says that there are two ways this can be denied: {1} we can say p’s negation holds, “¬p holds”, written as “+(–p),” or {2} we can say p fails to hold, “p does not hold”, written as and “– (+p)”. “He also claimed that the three cases excluded any other possibility so that either +p or +(–p) or –(+p), quartum non datur.” These correspond to the ways an intention can be fulfilled. Suppose that we have the proposition p: “the book is on the table”. {1} Fulfillment [Erfüllung], +p, would be that we perceive the table and see that the book is in fact on it; {2} frustration [Enttäuschung], +(–p), would be that we see the table and the book is not on it. In this case, there would be a conflict [Widerstreit]; and {3} nonfulfillment, –(+p), would be that we see neither the table nor the book. In this case, there is no conflict.]
[ditto]
The next contribution to a clarification of intuitionistic logic came from the philosophical analysis proposed by O. Becker. Since in 1931 Heyting gave an in- | terpretation of intuitionistic logic that appealed to Becker’s phenomenological interpretation of intuitionistic logic found in the 1927 book Mathematische Existenz, it is worthwhile to describe Becker’s approach. Becker’s interpretation rests on Husserl’s theory of judgments as exposed in the Logical Investigations (1900, 1913). Becker begins by remarking that there are two possible ways of denying the proposition “p holds.” We can have “¬p holds” or “p does not hold.” More formally, he writes “+p,” “+(–p),” and “– (+p).” He also claimed that the three cases excluded any other possibility so that either +p or +(–p) or –(+p), quartum non datur. In order to give a concrete interpretation of the situation, Becker interprets the three cases as fulfillment [Erfüllung], frustration [Enttäuschung], and nonfulfillment of an intention. Consider the proposition “the book is on the table” and call it p. To the case +p corresponds a fulfillment, given for instance in perception, of (l) the intended table in question and (2) of the state of affairs that the intended book is on the table. +(–p) corresponds to a situation in which the table is seen but the book is not on it. Finally –(+p) corresponds to a situation in which, for instance, neither the table nor the book is seen. The second case, unlike the last, gives a positive experience of a “conflict” [Widerstreit]. In the mathematical realm Becker translates the above by means of various examples involving becoming free choice sequences and law-like sequences.
(277-278)
[Truth and Falsity in Intuitionistic Logic, According to Becker]
[Becker defines truth and falsity in intuitionistic logic in the following way: “intuitionistic logic does not distinguish between ‘true’ and ‘false’ but between ‘true’ and ‘absurd.’ In this context ‘true’ means: actually provable (constructively), and absurd: ‘provably contradictory’ (from the phenomenological point of view one can in principle say: true = there is the synthesis of the fulfillment of the judgment intention, the agreement between what is intended and what is perceived; ‘absurd’: = there is the ‘synthesis’ of the frustration of the judgment intention, the ‘synthesis’ of the conflict.... Clearly there is no complete disjunction, in the sense of the tertium non datur, between fulfillment and frustration, agreement and conflict. (Becker 1927, p. 775)” (278). (Now take the book and table example again. Suppose we do not see that the book is on the table, that is, –(+p). Now suppose instead that we do not see that the book is not on the table, or –(–p). What, phenomenologically speaking, is the difference? There is no difference between the experiences of failing to see that the book is on the table compared with failing to see that the book is not on the table. Becker found this problematic, because the quartum non datur is +p or +(–p) or –(+p) and Wavre says that in intuitionistic logic we cannot have (p ∨ ¬p ∨ ¬¬p), but here Becker thinks that we should have the equivalent of ¬¬p as –(–p).) His solution for this was not satisfactory.]
[ditto]
The appendix (1927, pp. 335-40) contains several interesting reflections on the issue of the compatibility of the phenomenological interpretation with the Brouwerian interpretation. Becker gives a clear interpretation of the meaning of true and false in intuitionistic logic:
First of all it must be remarked that intuitionistic logic does not distinguish between “true” and “false” but between “true” and “absurd.” In this context “true” means: actually provable (constructively), and absurd: “provably contradictory” (from the phenomenological point of view one can in principle say: true = there is the synthesis of the fulfillment of the judgment intention, the agreement between what is intended and what is perceived; “absurd”: = there is the “synthesis” of the frustration of the judgment intention, the “synthesis” of the conflict.... Clearly there is no complete disjunction, in the sense of the tertium non datur, between fulfillment and frustration, agreement and conflict. (Becker 1927, p. 775)
This was at the source of the quartum non datur stated above. However, Becker remarks that Brouwer and Wavre seem flatly to deny this quartum non datur. The problem arises as follows. Becker asserts that phenomenologically –(+p) is equivalent to –(–p). But Wavre in his article (1926a, p. 72) remarked that intuitionistically we do not have (p ∨ ¬p ∨ ¬¬p). In order to avoid the conflict with the phenomenological interpretation, Becker interprets the third disjunction in his quartum non datur principle as ¬( p ∨ ¬p), that is, neither p nor ¬p is given. This, he claims, is in accord with intuitionistic principles. However, he was wrong in his claim since (p ∨ ¬p ∨ ¬(p ∨ ¬p)) is not intuitionistically valid. The principle is equivalent to the claim that if one rejects the principle of the excluded middle, then one has to accept its negation. It is unfortunate that after making such a good start in distinguishing the two meanings of negation, classical and intuitionist, Becker fell prey to the same confusion he was trying to clarify.
(278)
Becker, O., 1927, Mathematische Existenz, Jahrbuch für Philosophie und phämomenologische Forschung 8, pp. 439-809.
(284)
Wavre, R., 1926a, Logique formelle et logique empiriste, Revue de Metaphysique et de Morale 33, pp. 65-75.
Wavre, R., 1926b, Sur le principe du tiers exclu, Revue de Metaphysique et de Morale 33, pp. 425-30.
(285)
[Becker and Intuitionistic Logic Calculus]
[“Becker managed to ground all the principles in Wavre’s list according to his phenomenological interpretation. At the end of the appendix he also stated the problem of finding a calculus for intuitionistic logic” (279).]
[ditto]
The quartum non datur was to emerge again as a problem in the debate started | by Barzin and Errera to which I will soon tum. There is no need to list here in detail Becker’s phenomenological interpretation of the principles stated by Wavre and the interpretation of double negation. Suffice it to say that Becker managed to ground all the principles in Wavre’s list according to his phenomenological interpretation. At the end of the appendix he also stated the problem of finding a calculus for intuitionistic logic.
(278-279)
[Barzin & Errera’s “Tierce” Value and Their Failure to Critique Intuitionistic Logic ]
[Regarding the formulation of a calculus for intuitionistic logic, early on there were detractors. In 1927, Barzin and Errera argued that intuitionistic logic has a third value, “tierce,” written as “p′” and that on account of it and the semantics of intuitionism, the system leads to formal contradictions regarding the truth values. But their proofs involve using principles that are classically valid but not intuitionistically valid, so their attempt fails.]
[ditto]
But could there be such a calculus? Not everybody agreed that it was possible consistently to develop a Brouwerian logic. In particular Barzin and Errera 1927 made the claim that Brouwerian logic was inconsistent, thereby starting a long debate on intuitionistic logic. It will not be possible here to survey the numerous contributions to this debate, and we have to refer the reader to Thiel 1988 and Franchella 1995 for an overview. I will simply mention the objections raised by Barzin and Errera and expose Church’s and Glivenko’s answers to their claims. Barzin and Errera interpreted Brouwer’s position as claiming that there are propositions that are neither true nor false. These propositions are “tierce.” Their aim was to show that assuming a “tierce” led to formal contradictions.5 The strategy followed by Barzin and Errera was that of assuming the principles of intuitionistic logic and the principle of quartum non datur for a “tierce.” If we denote “p is tierce” by “p′,” then the principle of quartum non datur states “p ∨ ¬p ∨ p′.” Under this assumption their aim was to show that one could prove the collapse of the truth values, that is, that in the calculus the same proposition could be true and “tierce,” or “tierce” and false. In particular, they provided proofs that showed that if a proposition is “tierce,” then it is false (1927, p. 67) and that if a proposition is true, then it is “tierce” (1927, p. 68). It could be objected to their proof that in order to obtain their desired conclusions, p′ → ¬p and p → p′, they made use of a law that is classically but not intuitionistically valid, that is, ¬(p & q) → (¬p ∨ ¬q).6 Clearly, it would have been essential to their goals to make sure that only “intuitionistically” acceptable principles should appear in the proof. However, even granting the proof, it was not clear that the conclusion established their claim as to the impossibility of a logic with a third value.7
(279)
5. “L’objection que nous faisons a M. Brouwer est d’une autre nature: elle veut établir qu’il est impossible de raisonner en admittant un tiers, sans tomber aussitôt dans une contradiction que nous allons tacher de mettre en lumière” (Barzin, Errera 1927, p. 60).
6. This was remarked in Thiel 1988.
7. Indeed, the consistent developments of many-valued logics is already found in 1920 in Łukasiewicz, but none of the participants in the debate mention his work.
(283)
Barzin, M., and Errera, A., 1927, Sur la logique de M. Brouwer, Académie Royale de Belgique, Bulletin 13, pp. 56-71.
(283)
[Church’s Response to Barzin & Errera]
[In 1928, Church, in his “On the Law of the Excluded Middle”, reviews Barzin & Errera’s criticisms and makes the following three claims: {1} Dropping the law of excluded middle alone will not result in contradictions. {2} Barzin & Errera’s criticisms use reductio ad absurdum argumentation. But reductio arguments use the law of excluded middle, so these criticisms will not work for intuitionists who reject that law. And {3} Church incorrectly says that the “tierce” value being neither true nor false breaks the law of contradiction along with the law of excluded middle.]
[ditto]
In “On the Law of the Excluded Middle” (1928) Church gave a clear analysis of the situation by making the following three points. First of all, Church emphasized that if one drops the law of the excluded middle, then only a subset of the previously provable theorems can be proved, and thus no contradiction can emerge, unless the calculus we began with was already inconsistent. Thus the only possibility for the emergence of a contradiction is assuming a principle that contradicts the law of the excluded middle. The second point argues that the argument by Barzin and Errera is not effective against those who simply refuse to accept the excluded middle:
The method of the argument [by Barzin and Errera] is the method of reductio ad absurdum. It is assumed that if the law of the excluded middle is not accepted, then it must be explicitly denied by asserting the existence of tiers [sic] propositions, and on this basis contradictory results are obtained. This argument is clearly not effective against one who merely omits the law of the excluded middle from his system of logic without assuming any contrary principle, because the insistence that one who refuses to accept a proposition must deny it can be justified only by an appeal to the law of the excluded middle, the very principle in doubt. The method | of reductio ad absurdum, in fact, necessarily employs the law of excluded middle and cannot be used against one who does not admit this law. (1928, p. 77)
Finally, even if one accepts the existence of “tierce” propositions, it does not follow that Barzin and Errera are correct in their alleged proof of the inconsistency of the logic so obtained. This only follows if one accepts the quartum non datur. However, this principle is justified by interpreting the “tierce” proposition as one that is neither true nor false. But this definition is, according to Church, contradictory:
It is not possible, as an alternative to the law of the excluded middle, to assert that some proposition is neither true nor false, because by so doing not only the law of the excluded middle would be denied but also the law of contradiction. In fact, to assert that a proposition p is not true and is also not false is to assert at once not-p and not-(not-p) and consequently to assert that not-p is both true and false. (1928, p. 75)
However, this does not follow, and Church’s faux pas shows the intricacies of the conceptual issues involved in this debate.
(279-280)
Church, A., 1928, On the law of the excluded middle, Bulletin of the American Mathematical Society 34, pp. 75-78.
(284)
[Church Against Quartum non datur]
[Church did not see any reason for accepting the quartum non datur.]
[ditto]
Thus Church defended the possibility of a logic with “tierce” propositions. However, he recognized that if the concept of “tierce” is admitted, and together with it the quartum non datur, then the argument by Barzin and Errera is correct. But he saw no reason for accepting the quartum non datur.
(280)
[Glivenko’s Showing Intuitionistic Logic is Not Three-Valued]
[Glivenko in a 1928 paper shows that Brouwerian intuitionistic logic is not a three-valued logic, so the use of “tierce” propositions are invalid.]
[ditto]
Glivenko’s contribution to this debate (1928) consists in his claim that Brouwerian logic is not a three-valued logic [logique tripartite], that is, that the introduction of “tierce” propositions in Brouwerian logic is illegitimate. Starting from acceptable intuitionistic principles, he proves the following propositions:
1. ¬¬(¬p ∨ p)
2. ¬¬¬p → ¬p
3. ((¬p ∨ p) → ¬q) → ¬q
In order to show that in Brouwerian logic one could not admit a “tierce,” Glivenko argued as follows. If p is false, then its “tierce” is also false, that is, ¬p → ¬p′; and if p is true, its “tierce” is false, that is, p → ¬p′. By using the intuitionistically valid principle (VIII) to the effect that (p → r) → ((q → r) → ((p ∨ q) → r)), Glivenko was able to deduce, appealing to VIII and 3, that ¬p′.
(280)
Glivenko, V., 1928, Sur la logique de M. Brouwer, Académie Royale de Belgique, Bulletin 14, pp. 225-28.
(284)
[Glivenko and Interpreting Classical into Intuitionistic Logic]
[Glivenko in a 1929 paper provides “the first seeds of a development that will yield a long series of interpretations of classical logic into intuitionistic logic known as double negation interpretations or negative translations” (280-281).]
[ditto]
I shall leave now the debate provoked by Barzin and Errera to pursue the more technical contributions to intuitionistic propositional logic due to Glivenko, Heyting, and Kolmogorov. Let us begin with Glivenko 1929. If we ignore Kolmogorov 1925, which remained unknown until later, Glivenko 1929 contains the first seeds of a development that will yield a long series of interpretations of classical logic into intuitionistic logic known as double negation interpretations or negative translations (Kolmogorov 1925, Gödel 1933a, Gentzen 1933).8 Apart from some interesting additions to the axioms he had adopted in the previous article, the main two theorems of this paper can be given in Glivenko’s clear words:
1. If a certain expression in the logic of propositions is provable in classical logic, it is the falsity of the falsity of this expression that is provable in Brouwerian logic.
2. If the falsity of a certain expression in the logic of propositions is provable in classical logic, that same falsity is provable in Brouwerian logic. (1929, p. 301)
Glivenko’s work cannot be considered a translation of classical logic into intuitionistic logic, but it certainly paved the way to that result. Although Glivenko was Russian, he does not seem to have been aware of Kolmogorov 1925 until after he had completed his 1929 paper. He mentions Kolmogorov’s article in a letter to Heyting dated October 13, 1928 (the letter is published in Troelstra 1990).9
(280-281)
8. For a contemporary exposition see Troelstra and van Dalen 1988, Chap. 2, Sect. 3. For historical information on Kolmogorov 1925, Gödel 1933a, and Gentzen 1933, see Wang 1967, Troelstra 1986, and Gentzen 1969, respectively.
9. The correspondence between Heyting and Glivenko is published in Troelstra 1990.
(283)
Glivenko, V., 1929, Sur quelques points de la logique de M. Brouwer, Académie Royale de Belgique, Bulletin 15, pp. 183-88. English translation: this volume, Chapter 22.
(284)
Kolmogorov, A. N., 1925, O principe tertium non datur, Matematiceskij Sbornik 32, pp. 646-67. English translation in J. van Heijenoort, ed., From Frege to Gödel, Harvard University Press, Cambridge (Mass.), 1967, pp. 416-37.
(284)
Gödel, K., 1933a, Eine Interpretation des intuitionistischen Aussagenkalküls, Ergebnisse eines mathematischen Kolloquiums, Heft 4, pp. 39-40. English translation in Gödel 1986.
(284)
Gödel, K., 1986, Collected Works I, S. Feferman et al., Eds., Oxford University Press, Oxford.
(284)
Gentzen, G., 1933, Uber das Verhältnis zwischen intuitionistischer und klassischer Logik. First published in German in 1974. English translation in Gentzen 1969.
(284)
Gentzen, G., 1969, Collected Papers, M. E. Szabo, Ed., North Holland, Amsterdam.
(284)
Troelstra, A. S., and van Dalen, D., 1988, Constructivism in Mathematics. An Introduction, Vol. I, North-Holland, Amsterdam.
(285)
Wang, H., 1967, Introductory Note to Kolmogorov 1925, in J. van Heijenoort, ed., From Frege to Gödel, Harvard University Press, Cambridge (Mass.), 1967, pp. 414-16.
(285)
Troelstra, A. S., 1986, “Introductory note to Gödel 1933e,” in Gödel 1986, pp. 282-87.
(285)
Troelstra, A. S., 1990, On the early history of intuitionistic logic, in Mathematical Logic, P. P. Petkov, Ed., Plenum Press, New York and London, pp. 3-17.
(285)
[Heyting and the Formalization of Intuitionistic Logic]
[Around the same time, Heyting was formalizing the principles of intuitionistic logic.]
[ditto]
At the same time, Heyting had been working on a formalization of the principles of intuitionistic logic. The occasion for the paper was a prize question published in 1927 by the Dutch Mathematical Association on the logic of Brouwerian mathematics. Heyting was awarded the prize in 1928, and his paper appeared in 1930. There were actually three papers, the first one of which, and the only one presented here, was concerned with the intuitionistic propositional calculus (for details on first-order intuitionistic logic, see Troelstra 1990). The other two papers dealt with the formalization of intuitionistic mathematics.
(281)
Troelstra, A. S., 1990, On the early history of intuitionistic logic, in Mathematical Logic, P. P. Petkov, Ed., Plenum Press, New York and London, pp. 3-17.
(285)
[Heyting’s Elaborations on His Insights]
[In a letter to Becker from 1933, Heyting explains some of his insights into intuitionistic logic and how he came upon them.]
[ditto]
In a letter to Becker, dated September 23, 1933, Heyting described how he found his axiomatization simply by going through the axioms and theorems of Principia Mathematica and including the “admissible” ones into a system of independent axioms (for a list of the axioms, see the appendix to Heyting 1930b). The letter contains some other interesting reflections. For example, Heyting claims that “it is in principle impossible to encompass with certainty in a formal system all the ‘admissible’ modes of inference” (original German in Troelstra 1990, p. 8). He also distinguished between two different interpretations of the intuitionistic calculus, in terms of problems and of expectations.
(281)
Heyting, A., 1930b, Die formalen Regeln der intuitionistischen Logik, Sitzungsberichte der Preussischen Akademie der Wissenschaften, pp. 42-56. English translation: this volume, Chapter 24.
(284)
Troelstra, A. S., 1990, On the early history of intuitionistic logic, in Mathematical Logic, P. P. Petkov, Ed., Plenum Press, New York and London, pp. 3-17.
(285)
[Heyting’s Account of the Logical Connectives and His Use of Becker’s Phenomenological Interpretation of Intuitionistic Logic]
[In other papers Heyting gives the interpretations for logical connectives in intuitionistic logic. There we also see elements of Becker’s phenomenological interpretation.]
[ditto]
In the 1930b paper the “admissible” principles were only stated, and Heyting was not explicit on what the interpretation of the logical connectives in intuitionistic logic was. Heyting 1930a and 1931 provide an explicit interpretation for the connectives ¬, and “or.”10 Let us look at 1930a. Heyting says that a proposition p expresses a problem or an expectation:
A proposition p like, for example, “Euler’s constant is rational,” expresses a problem, or better yet, a certain expectation (that of finding two integers a and b such that C = a/b), which can be fulfilled [réalisée] or disappointed [déçue]. (1930a, p. 307)
The interpretation in terms of expectations reminds one of Becker’s phenomenological interpretation for intuitionistic logic. Although Becker and Heyting corresponded about matters of intuitionistic logic in 1933, I do not know whether they had any personal contact at the time of Heyting’s first attempts at providing an interpretation of intuitionistic logic. However, Heyting had certainly read Becker’s Mathematische Existenz, since in 1931 he quotes it approvingly. Heyting 1931 also reveals that the phenomenological interpretation was very much the one favored by Heyting at this stage:
We conclude our treatment of the construction of mathematics in order to say something about the intuitionist propositional calculus. We here distinguish between propositions and assertions. An assertion is the affirmation of a proposition. A mathematical proposition expresses a certain expectation. For example, the proposition “Euler’s constant C is rational” expresses the expectation that we could find two integers a and b such that C = a/b. Perhaps the word “intention,” coined by the phenomenologists, expresses even better what is meant here .... The affirmation of a proposition means the fulfillment of an intention. (1931, pp. 58-59)
| Becker is explicitly quoted in connection with the interpretation for negation:
A logical function is a process for forming another proposition from a given proposition. Negation is such a function. Becker, following Husserl, has described its meaning very clearly. For him negation is something thoroughly positive, viz. the intention of a contradiction contained in the original intention. The proposition “C is not rational,” therefore, signifies the expectation that one can derive a contradiction from the assumption that C is rational. (1931, p. 59)
As for disjunction, he observes that a proposition like “p ∨ ¬p” expresses the expectation of a mathematical construction that will either prove p or ¬p.
(281-282)
10. The explicit interpretation of the intuitionistic meaning of implication is given in correspondence with Freudenthal and in print in 1934.
(283)
Heyting, A., 1930b, Die formalen Regeln der intuitionistischen Logik, Sitzungsberichte der Preussischen Akademie der Wissenschaften, pp. 42-56. English translation: this volume, Chapter 24.
(284)
Heyting, A., 1930a, Sur la logique intuitionniste, Académie Royale de Belgique, Bulletin 16, pp. 957-63. English translation: this volume, Chapter 23.
(284)
Heyting, A., 1931, Die intuitionistische Grundlegung der Mathematik, Erkenntnis 2, pp. 106-15. English translation in P. Benacerraf and H. Putnam, Eds., Philosophy of Mathematics, 2nd ed., Cambridge University Press, Cambridge (Mass.) 1983, pp. 52-61.
(284)
[Other Features of Heyting’s Formalization]
[Heyting also says that we cannot simply identify “ ‘p is true’ (in the intuitionistic sense) with ‘p is provable’,” because we need “the observation of an empirical fact, that is, of the realization of the expectation expressed by the proposition p. Here, then, is the Brouwerian assertion of p: It is known how to prove p. (1930a, p. 307)” (282).]
[ditto]
In addition to containing the above interpretation for the intuitionistic connectives ¬ and “or,” Heyting 1930a and 1931 also contain several interesting features. For example, Heyting argues against Levy, who had identified “p is true” (in the intuitionistic sense) with “p is provable.” He objects that Levy’s distinction does not satisfy the intuitionistic demands:
One does not escape this criticism by replacing, with Mr. Levy, “p is true” by “p is provable,” since this last sentence, being equivalent to “there exists a proof of p,” implies again the idea of transcendent existence. To satisfy the intuitionistic demands, the assertion must be the observation of an empirical fact, that is, of the realization of the expectation expressed by the proposition p. Here, then, is the Brouwerian assertion of p: It is known how to prove p. (1930a, p. 307)
Heyting also distinguishes carefully between the statement p and p is provable (denoted by +p). However, at the end of Heyting 1931 he claims that developing the intuitionistic calculus with the function + would lead to useless complications (see pp. 60-61) and that his calculus should be interpreted as valid only for propositions of the form +p.11
(282)
11. Heyting’s position was influenced by an exchange with Freudenthal. See Troelstra 1990 and Troelstra 1983.
(283)
Heyting, A., l930a, Sur la logique intuitionniste, Académie Royale de Belgique, Bulletin 16, pp. 957-63. English translation: this volume, Chapter 23.
(284)
Heyting, A., 1931, Die intuitionistische Grundlegung der Mathematik, Erkenntnis 2, pp. 106-15. English translation in P. Benacerraf and H. Putnam, Eds., Philosophy of Mathematics, 2nd ed., Cambridge University Press, Cambridge (Mass.) 1983, pp. 52-61.
(284)
Troelstra, A. S., 1990, On the early history of intuitionistic logic, in Mathematical Logic, P. P. Petkov, Ed., Plenum Press, New York and London, pp. 3-17.
(285)
Troelstra, A. S., 1983, Logic in the writings of Brouwer and Heyting, in V. M Abrusci, E. Casari and M. Mugnai, Eds., Atti del convegno internazionale di storia della logica, San Gimignano, 4-8 Dicembre 1982, CLUEB, Bologna, pp. 193-210.
(285)
[Heyting and Kolmogorov on Expectation and Problem]
[For Heyting and Kolmogorov, a proposition p can be interpreted either as an expectation or a problem.]
[ditto]
Let me conclude this introduction with a few words about Kolmogorov’s interpretation of intuitionistic logic. We have seen that Heyting mentioned the possibility of interpreting a proposition p as a problem, although he seems to have favored the interpretation in terms of expectations. As Troelstra (1990, p. 7) remarks, Heyting and Kolmogorov seem to have considered the interpretations in terms of problems and expectations as distinct. Indeed, in his introduction to intuitionism (1934), Heyting describes both interpretations, although he will later consider them as essentially equivalent.
(282)
Troelstra, A. S., 1990, On the early history of intuitionistic logic, in Mathematical Logic, P. P. Petkov, Ed., Plenum Press, New York and London, pp. 3-17.
(285)
Heyting, A., 1934, Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Springer, Berlin. Extended French translation, Les Fondements des Mathematiques. Intuitionisme, Théorie de la Démonstration, Gauthier-Villars, Paris, 1955.
(284)
[Kolmogorov and the Problem Interpretation]
[Kolmogorov in 1932 explains the problem interpretation: “If a and b are two problems, then a & b designates the problem ‘to solve both problems a and b,’ while a ∨ b designates the problem ‘to solve at least one of the problems a and b.’ Furthermore, a ⊃ b is the problem ‘to solve b provided that the solution for a is given’ or, equivalently, ‘to reduce the solution of b to the solution of a’ [ ... ] ¬a designates the problem ‘to obtain a contradiction provided that the solution of a is given.’ (1932, p. 329)” (282).]
[ditto]
Kolmogorov 1932 first introduces the notion of problem by means of examples and then proceeds to delineate a logic of problems:
If a and b are two problems, then a & b designates the problem “to solve both problems a and b,” while a ∨ b designates the problem “to solve at least one of the problems a and b.” Furthermore, a ⊃ b is the problem “to solve b provided that the solution for a is given” or, equivalently, “to reduce the solution of b to the solution of a” [ ... ] ¬a designates the problem “to obtain a contradiction provided that the solution of a is given.” (1932, p. 329)
Kolmogorov then set up a system of axioms for the calculus of problems and remarked that “the calculus of problems is formally identical with the Brouwerian intuitionistic logic, which has been recently formalized by Mr. Heyting.” However, in a note added in proof, Kolmogorov pointed out that although his interpretation was similar to the one given by Heyting in 1931, the distinction between propositions and problems was missing in Heyting’s article.
(282-283)
Kolmogorov, A. N., 1932, Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift 35, pp. 58-65. English translation: this volume, Chapter 25.
(285)
[Summation]
[We have thus seen three major events in the history of intuitionistic logic: “Heyting had provided a complete formalization of intuitionistic logic, Glivenko had pointed the way to the negative interpretations to follow, and the combined work of Heyting and Kolmogorov had given an explicit formulation to what is now known as the BHK interpretation of intuitionistic logic” (283). ]
[ditto]
With the articles by Glivenko, Heyting, and Kolmogorov, three major events in the history of intuitionism had been accomplished. Heyting had provided a complete formalization of intuitionistic logic, Glivenko had pointed the way to the negative interpretations to follow, and the combined work of Heyting and Kolmogorov had given an explicit formulation to what is now known as the BHK interpretation of intuitionistic logic. In the years to follow many more results would be obtained, and we have to refer the reader to Troelstra and van Dalen 1988 for more information on the mathematical and metamathematical results obtained in the wake of the groundbreaking works of Brouwer, Glivenko, Heyting, and Kolmogorov.
(283)
From:
Mancosu, Paolo & Stigt, Walter P. van. (1989). “Intuitionistic Logic” In: From Brouwer to Hilbert: The Debate on the Foundations of Mathematics in the 1920’s, edited by Paolo Mancosu. Oxford: Oxford University.
No comments:
Post a Comment