The Turn to Heyting’s Formalized Logic and Arithmetic

1. Some early results

1. Intuitionistic propositional logic is not a finitely valued logic. Gödel (1932) showed that Heyting’s system for intuitionistic propositional logic cannot be conceived of as a finitely many-valued logic. Apparently unbeknown to Gödel, this confirmed a conjecture of Oskar Becker (1927: 775–777). Gödel’s result, which came soon after his incompleteness theorem, led Heyting to write to him,

   It is as if you had a malicious pleasure in showing the purposelessness of others’ investigations … In the sense of economy of thought this work is certainly useful, and in addition to that comes the particular beauty of your short proof. [Heyting to Gödel, letter dated 24 and 26 November 1932. (Gödel 2003a: 67)]

2. Peano Arithmetic is translatable into Heyting Arithmetic. A seminal theorem was obtained independently by Gödel (1933e) and by Gentzen (withdrawn upon learning of Gödel’s paper): There is a translation \('\) from PA to HA such that

   \[\textbf{PA} \vdash A \Leftrightarrow \textbf{HA} \vdash A'\]

   (Gödel and Gentzen actually used Herbrand’s axioms for the natural numbers (Herbrand 1931), but that is immaterial here.) The same proofs serve to show that the same result holds for pure predicate logic. This completes and generalizes Kolmogorov’s result from 1925, which at the time was known to neither Gentzen nor Gödel (Gödel does cite Glivenko 1929). Gödel concluded that

   the system of intuitionistic arithmetic and number theory is only apparently narrower than the classical one, and in truth contains it, albeit with a somewhat deviant interpretation. (Gödel 1933e: 37 [1986: 295])

   Heyting replied that “for the intuitionist, the interpretation is what is essential” (Heyting 1934: 18; translation mine). Later Gödel became, as Kreisel put it, “supersensitive about differences in meaning” (Kreisel 1987a: 82). The Gödel-Gentzen translation had an immediate application to the foundational debate, in which besides the notion of existence the status of PEM had been the main issue (Hesseling 2003): the embedding of PA into HA shows that PA is consistent if and only if HA is. As Gödel observed,

   The above considerations, of course, provide an intuitionistic consistency proof for classical arithmetic and number theory. This proof, however, is not “finitary” in the sense in which Herbrand, following Hilbert, used the term. (Gödel 1933e: 37–38 [1986: 295])^[31]

   Indeed, according to Bernays (1967: 502), it was this fact that made it clear that intuitionism is stronger than Hilbert’s finitism.

3. Interpreting intuitionistic logic in a classical provability logic, Gödel (1933f) presented a mapping \('\) of intuitionistic propositional logic PC to classical modal logic S4 such that

   \[ \textbf{IPC} \vdash A \Rightarrow \textbf{S4} \vdash A' \]

   For more details on this result, see the section Gödel’s Work in Intuitionistic Logic and Arithmetic of Kennedy 2007, as well as Artemov 2001.

   As pointed out by Troelstra (Gödel 1986: 299), at the time Gödel certainly knew the content of Heyting 1931. He had attended the Königsberg conference (where Heyting had presented that paper) and had published a review (Gödel 1932f) of the printed version. In that paper, Heyting had introduced a provability operator, but considered it redundant given the intuitionistic conception of truth as provability (see below, section 5.1).^[32]

4. Consider the following two properties:
   • the Disjunction Property (DP): if \(\vdash A \vee B\), then \(\vdash A\) or \(\vdash B\);
   • the Explicit Definability property (EP): if \(\vdash \exists x P(x)\), then \(\vdash P(t)\) for some term \(t\)

   DP for intuitionistic propositional calculus was stated by Gödel (1932: 66 [1986: 225]), who did not give a proof. A proof was given for intuitionistic predicate logic by Gentzen (1934). As Troelstra and van Dalen (1988: 175) observe, the same method (cut-elimination) yields ED for intuitionistic predicate calculus. For Heyting Arithmetic, see Kleene 1945 (section 8) and Kleene 1952 (theorem 62b).

5. The intuitionistic connectives are not interdefinable: none of \(\rightarrow , \wedge , \vee , \neg\) can be defined in terms of the others. Heyting had stated this in Heyting 1930: 44 [Mancosu 1998: 312], but without giving a proof. A proof was published by Wajsberg (1938) and (independently and by different methods) by McKinsey (1939).

2. Mathematical interpretations and model-theoretic semantics

Various mathematical interpretations (in the sense explained in section 1.2) of formalized intuitionistic logic and arithmetic have been proposed. Above we saw Gödel’s translation of intuitionistic propositional logic into the classical modal logic S4 from 1933; further examples are Kleene’s realizability (Kleene 1945), and Gödel’s Dialectica Interpretation (Gödel 1958, 1970, 1972).

Such mathematical interpretations are not meaning explanations. There are two arguments. The first is that, in a context where formal systems are arithmetized, interpretability results are established wholly within mathematics (e.g., Joosten 2004). But then no contact at all is made with the concepts that figure in meaning explanations, which have to do with our cognitive capacities, such as those of effecting mathematical constructions or those of understanding, learning, and using a language. The second, more general argument is due to Sundholm (1983: 159). Here we consider \(A\) and its interpretation \(A'\) not as syntactical objects but as meaningful propositions. Then the argument is that, by whatever means one correlates a mathematical proposition \(A'\) to a mathematical proposition \(A\), it makes sense to ask whether the propositions \(A\) and \(A'\) are equivalent. On the other hand, it does not make sense to ask whether the proposition \(A\) is equivalent to a specification of what one has to know in order to understand \(A\) and use it correctly; for example, that specification remains the same whether \(A\) is true, false, or undecided. But then \(A'\) cannot be a meaning explanation of \(A\).

It would therefore be a mistake to see in mathematical interpretations of intuitionistic systems ways to make the Proof Interpretation “rigorous” or “precise”. The difference is not one of degree but of kind.^[33] The point is general, and it makes no difference if the interpreting theory \(V\) is intuitionistic.^[34] On the other hand, it is not at all ruled out that for an interpreting theory \(V\) itself an explanation can be given that is arguably superior to the Proof Interpretation in some respect; this was Gödel’s philosophical aim for his Dialectica Interpretation.

A related point can be made about model-theoretic semantics for a(ny) logic (Dummett 1973: 293–294): these map formulas to mathematical objects, without there being an intrinsic connection between those objects and the concepts related to our understanding and use of a language. By itself, therefore, such a semantics does not contribute to a meaning explanation. (The first argument on mathematical interpretations, above, is essentially the same as this one.) But for metamathematical purposes, such model-theoretic semantics have proved extremely valuable. Note that Heyting (1930) used model-theoretic semantics to show the independence of his axioms for propositional logic. A wide variety of model-theoretic semantics for intuitionistic systems has been developed since, beginning with the topological ones of Stone (1937) and Tarski (1938). Of the remaining ones, among the best known are Beth models (Beth 1956), Kripke models (Kripke 1965), and topos models. For Kripke models, see the section Kripke semantics for intuitionistic logic of Moschovakis 2007; for other models and further references, see Kleene and Vesley 1965: 6 and Artemov 2001.