Intuitionism and the liar paradox (Q448337)

This is a paper concerned with the relation between the notion of an informal mathematical proof (IMP), as it is understood in traditional intuitionism, and the (provable) liar paradox (PLP). According to the author, PLP reveals a ``very serious problem'' for the traditional intuitionistic understanding of IMP. His way out is the formation of a new notion of IMP, which obeys some crucially different principles than the traditional one and blocks the contradiction generated by PLP. Moreover, the author uses this new notion of IMP to resolve the classical (truth-related) liar paradox (TLP). The author begins his philosophical analysis with the recognition that IMP cannot be modeled, or fully captured, by the notion of a formal mathematical proof (FMP), since for any formal system \(S\) modeling informal reasoning there is a formula for which we possess an IMP but not an FMP within \(S\). Although IMP can only be partially modeled by FMP, the author assumes that the study of IMP is meaningful, otherwise ``mathematics is nothing but a meaningless formal game with symbols'' and that ``we need to have a general semantic notion of proof validity''. We denote this philosophical assumption of the author by PA1. The author concludes that traditional IMP is an ``indefinitely extendible concept'' (IEC), a notion of Dummett, and since Dummett has shown that many other concepts, like ``set'', ``truth'', and ``definition'', are IEC, ``we ought to be comfortable'' with the concept IMP, ``despite the fact that it is only capable of partial formalization''. The second philosophical assumption of the author (which we denote here by PA2), and crucial to the rest of his study, is that the paradoxical character of the sentence (the author obtains a contradiction even within intuitionistic logic) \(L =\) ``This sentence is not provable'' is ``a very serious problem'' for IMP. He considers that the generated contradiction proves that IMP, as it is ``characterized in traditional intuitionism'', is incoherent. The author stays faithful to PA1 by developing, because of his PA2, a new notion of IMP. He considers the ``intuitionist's mistake'' with regard to IMP to be the decidability of proof validity and assumes (this is what we call the author's third philosophical assumption PA3) that proof validity is not decidable. The author's new notion of IMP obeying PA3 is not IEC, since that would imply decidability, but, as he says, it is a heuristic concept (HC). Although the understanding of what it means to fall under IEC does not change by producing new individuals falling under it, this is not the case for HC. While intuitionistic logic is for Dummett the appropriate logic for reasoning about IEC, like the traditional IMP, the author elaborates the justification of what we call here his fifth philosophical assumption PA5, namely that ``minimal logic is suitable for reasoning about HC, in particular for reasoning about provability''. The author justifies his restriction to minimal logic by ascribing a circularity in the standard justification of the ``ex falso quodlibet'' (EFQ), the only intuitionistic logical principle not accepted within minimal logic. The author's argument is based on the assumption that we do not know that there is no IMP of \(0 = 1\) (and this we call the author's fourth philosophical assumption PA4). Using PA1--PA5, the author shows how the contradiction of LP cannot be deduced. Finally, the author equates truth with provability in order to resolve the standard liar paradox the way he resolves PLP. The reader of this paper will benefit from a correlation of the author's arguments to the corresponding, but not mentioned by the author, intuitionistic bibliography. Besides, intuitionism is not a single point of view and its reaction to LP is not uniform. Brouwer had always considered IMP more important, or fundamental, than FMP, therefore he strongly believed in PA1 and he had never considered as a problem that IMP is not captured by FMP. For him, pure mathematical activity is pre-linguistic. But Brouwer would not accept PA2, since for him, IMP reflects a mathematical, non-linguistic construction. Since \(L\) lacks mathematical content, it cannot cause any problem for IMP. In his dissertation [On the foundations of mathematics. In: Collected works. Vol. 1: Philosophy and foundations of mathematics. Amsterdam-Oxford: North-Holland Publishing Company; New York: American Elsevier Publishing Company (1975; Zbl 0311.01021)], \textit{L. E. J. Brouwer} had a similar attitude towards even `more' mathematical antinomies. On the other extreme, \textit{N. D. Goodman}, in his paper [``A theory of constructions equivalent to arithmetic'', in: Intuitionism Proof Theory, Proc. Summer Conf. Buffalo N.Y. 1968, 101--120 (1970; Zbl 0212.31301)], elaborating previous ideas of Kreisel, used Curry's combinators to construct a self-referential sentence which asserts of itself that it is unprovable. He resolved the generated paradox through the so-called Kreisel-Goodman stratified theory of constructions \(\mathcal{C}\). Regarding the author's PA3 and the decidability of IMP as a ``mistake intuitionists have made'', the debate on the decidability of IMP within intuitionism is not new. Kreisel was an advocate of it (and, as rightly mentioned by the author, \textit{A. S. Troelstra} in his book [Principles of intuitionism. Berlin-Heidelberg-New York: Springer Verlag (1969; Zbl 0181.00504)] also was). But \textit{M. J. Beeson}, in his book [Foundations of constructive mathematics. Metamathematical studies. Berlin etc.: Springer-Verlag (1985; Zbl 0565.03028)], proved that his formal system C refutes the decidability of the truth-predicate and it is conservative over Heyting arithmetic. As Beeson mentions in the same book, p.~409, this result was already known to Goodman in the early 60s, whose theory of constructions satisfied the decidability of the proof-predicate largely due to the influence of Kreisel. The author's critique of the universal justification of EFQ (the author is very careful acknowledging many settings in which EFQ is valid) can be related to other kinds of critique of EFQ, even within intuitionism (see, e.g., \textit{M. van Atten}'s book [On Brouwer. Belmont, CA: Wadsworth/Thomson Learning (2004; Zbl 1072.03005)] and \textit{D. van Dalen}'s paper [``Kolmogorov and Brouwer on constructive implication, and the contradiction rule'', Russ. Math. Surv. 59, No. 2, 247--257 (2004); translation from Usp. Mat. Nauk 59, No. 2, 53--64 (2004; Zbl 1056.03039)]). Regarding the author's PA4, we only mention here that Brouwer, who never used EFQ in his intuitionistic work, justified the existence of no IMP of \(0 = 1\) in his dissertation, p.~159, as follows: ``in the linguistic accompaniment of mathematical constructed systems \(\ldots\) the sequence of sentences which follow one another logically will never produce contradictions since they accompany mathematical acts of construction''.