the inclusion of classical into intuitionistic logic

Abstract

The entry is a report of Gödel’s 1933 first proof of the consistency of classical arithmetic by means of an interpretation of the basic concepts of intuitionistic logic. The seminal theorem is Glivenko’s Theorem and full proofs of the theorems derived from Gödel’s translation function are provided. An attempt is made to clear some minor problems with Gödel’s original text. In spite of the provided continuity between the sections one can read most of them in isolation.

The inclusion of classical into intuitionistic logic

1 Background

Brouwer visited Vienna on March 10, 1928 when he delivered his lecture "Mathematik, Wissenschaft und Sprache". Members of the Vienna Circle were attending, among them Hans Hahn, from the Mathematical Institute.

One of the members of the Vienna Circle attending Brouwer’s lecture was Karl Menger. Menger did his Ph.D. with Hans Hahn and his Habilitation with Brouwer in Amsterdam. He remained a member of the Circle until he left Austria for the United States.

In 1932 Menger conducted a Colloquium in the Mathematical Institute in which on June 26 Kurt Gödel presented his first proof of the Consistency of classical number theory relative to intuitionistic number theory.

We give an overview of the main theorem and suggest two minor corrections.

2 The analogy from the generalized Glivenko theorem

1. Notation

   A. Classical propositional calculus ($K$):

   the symbols

   "$\sim$", "$\to$", "$\cdot$"

   denote the truth-functions negation, implication and conjunction, respectively.

   B. Intuitionistic propositional calculus ($I$):

   the symbols

   "$\mathrm{\neg }$", "$\wedge$"

   denote the intuitionistic connectives negation and conjunction, respectively.

2. Glivenko’s theorem

   Let $F$ be a well formed formula of $K$ which consists only of conjunctions and negations. If $F$ is valid in $K$ then it is demonstrable in $I$.

   This means that $F$ must have the form:

   $(\star \star )$     $\mathrm{\neg }{F}_1\wedge \mathrm{\neg }{F}_2\wedge \mathrm{\dots }\mathrm{\neg }{F}_n$.

   If the formula $(\star \star )$ is valid in $K$ then each $\mathrm{\neg }{F}_i$ is also valid. Glivenko proves that $\mathrm{\neg }{F}_i$ is provable in $I$, as we can see in Heyting (1930), pg. 43.

   In that case the whole formula $(\star \star )$ is also provable in $I$.

3. The generalized Glivenko’s theorem

   The set of valid formulas of $K$ is a subset of all valid formulas of $I$.

   To see this one translates a classically valid formula into a formula of $I$. The translations rules are the following:

   A. Negation: the classical function $\sim p$ has the translation $\mathrm{\neg }p$;

   B. Disjunction: the classical function $p\vee q$ has the translation:

   $\mathrm{\neg }(\mathrm{\neg }p\wedge \mathrm{\neg }q)$;

   C. Implication: the classical function $p\to q$ has the translation:

   $\mathrm{\neg }(p\wedge \mathrm{\neg }q)$;

   D. Conjunction: the classical function $p\cdot q$ has the translation:

   $p\wedge q$.

3 Configuration of Herbrand’s system

Gödel’s theme is to prove that for arithmetic and number theory one can also obtain a result analogous to the result obtained by Glivenko for the propositional calculus.

To achieve this we have to find translation rules such that the set of classically provable formulas becomes a subset of all intuitionistically valid formulas.

The supporting system used is Herbrand’s (1931) with the following configuration:

1. Primitive symbols:

   A. The functions of the classical propositional calculus

   B. Numerical variables: small Roman $x$, $y$, $\mathrm{\dots }$

   C. Universal quantifiers: $(\forall x)$, $(\forall y)$, $\mathrm{\dots }$

   D. Equality: "="

   E. Numerals: 0, 1, $\mathrm{\dots }$

   F. A countable set of functional symbols $f_i$, introduced according to Herbrand’s axioms.

   To each symbol one associates an integer $n_i$, which denotes the number of arguments of $f_i$.

2. Formulas:

   A. Numerical expression

   As a preliminary definition we have the recursive definition of numerical expression:

   • i) 0 and every numerical variable are numerical expressions;

   • ii) If $Z$ is a numerical expression $Z+1$ is a numerical expression;

   • iii) If $Z_1$, $\mathrm{\dots }$, $Z_n$ are numerical expressions then:

     $f(Z_1,\mathrm{\dots },Z_n)$

     is a numerical expression.

   B. Atomic formula

   An atomic formula is an equality, the terms of which are numerical expressions. Thus:

   $Z_i=Z_j$

   is an atomic formula.

   C. $Z$-formula

   • i) An atomic formula is a $Z$-formula;

   • ii) Numerical expressions that result from atomic formulas by means of the functions of the propositional calculus or by the use of quantifiers are $Z$-formulas.

3. Axioms:

   A. Herbrand’s axioms in particular from $A$ to $D$.

   B. Logical Axioms

   Three axioms are introduced with the following content:

   • Axiom E: [Rule of insertion]

     Every numerical expression that results from the insertion of a $Z$-formula in a tautology of the propositional calculus is an axiom.

   • Axiom F: [Dictum de omni]

     If $F(x)$ is a $Z$-formula and $Z$ is a numerical expression such that the variables of $Z$ are not bound in $F$, then all formulas of the pattern:

     $(\forall x)F(x)\to F(Z)$

     are axioms.

   • Axiom G: [Leibniz]

     If $F(x)$ is a $Z$-formula then all formulas of the pattern:

     $x=y\to F(x)\to F(y)$

     are axioms.

4. Rules of inference:

   A. Modus ponens

   From $A\to B$ and $A$ we are allowed to infer $B$.

   B. $\mathrm{\forall }$-Introduction in the implicatum

   If $x$ does not occur free in $A$ then from $A\to B$ we are allowed to infer $A\to (\forall x)B$.

4 Gödel’s translation mapping: the system H’

Heyting’s system used is to be found in "Die formalen Regeln der intuitionistischen Mathematik" (1930) with a few notation variants.

In this system small roman letters $x$, $y$, $\mathrm{\dots }$ are not numerical variables; they rather denote objects.

1. The translation mapping "$\mathrm{\prime }$":

   If $x,y,z$ are object variables from Heyting’s system, they will be translated into numerical variables by means of Gödel’s translation mapping "$\prime$" as $x^{\prime },y^{\prime },z^{\prime }$ being now variables for natural numbers.

   The notation is defined by the rules:

   A. ${(𝒳\wedge 𝒴)}^{\prime }\leftrightarrow {𝒳}^{\prime }\wedge {𝒴}^{\prime }$

   B. ${(𝒳\vee 𝒴)}^{\prime }\leftrightarrow \mathrm{\neg }(\mathrm{\neg }{𝒳}^{\prime }\wedge \mathrm{\neg }{𝒴}^{\prime })$

   C. ${(𝒳\to 𝒴)}^{\prime }\leftrightarrow \mathrm{\neg }({𝒳}^{\prime }\wedge \mathrm{\neg }{𝒴}^{\prime })$

   D. If $A(x^{\prime },y^{\prime },\mathrm{\dots })$ is a formula in which these variables occur free then:

   $[A(x^{\prime },y^{\prime },\mathrm{\dots })]\leftrightarrow [(x,y,\mathrm{\dots }\in \mathbb{N})\to A(x,y,\mathrm{\dots })]$

   E. If $(\forall x^{\prime })F(x^{\prime })$ is a formula then:

   $(\forall x^{\prime })F(x^{\prime })\leftrightarrow [(\forall x)(x\in \mathbb{N})\to F(x)]$

2. Translation preserves validity:

   The relevant formulas belong to $\mathrm{\S }5$ [of $H2$, on the basic definitions and inference rules] and $\mathrm{\S }6$ [of $H2$, on quantification). If in these formulas in the place of the variables we insert their translations the formulas remain valid, that is, translation preserves validity.

   Gödel says that in order to achieve a validity-preserving translation of Heyting’s formula 5.4 we have to substitute "$p\overline{\equiv }p$" by "$p^{\prime }\overline{\equiv }\mathbb{N}$".

   Now formula 5.4 says that the set of valid formulas is closed under substitution provided that:

   • i) For a propositional variable any expression can be inserted and

   • ii) For an object variable a symbolic expression $p$ can be inserted, if $p\overline{\equiv }p$ is a valid formula.

     We think that a more intuitive translation would be to follow the pattern of the rules i) and ii) above and propose instead:

     $(p^{\prime }\overline{\equiv }{p}^{\prime })\leftrightarrow [p\in \mathbb{N}\to p\overline{\equiv }p].$

3. Definition of arithmetical functions:

   A. The definition of a function by recursion is intuitionistically acceptable and it is Heyting’s method in 10.03 and 10.4.

   B. Herbrand’s axioms Group $C$ allow the introduction of functions $f_i(x_1,\mathrm{\dots },x_n)$ such that the computation of $f(x_1,\mathrm{\dots },x_n)$ is always possible for any $n$-tuple of numbers.

   Ex.: if a function $g(y)$ has already been introduced then we can define a new function $f(x)$ by recursion on $x$ with the following recursion equations:

   $f(0)=k$

   $f(x+1)=g(f(x)).$

   The axioms of Group $C$ and the axioms of Group $D$, which allow the introduction of universal quantifiers, are adjoined to $H$. The resulting system will be called $H^{\prime }$.

4. The $Z\mathbf{}Ã\mathbf{}\mathrm{¢}\mathbf{}â\mathbf{}\mathrm{‚}\mathbf{}\mathrm{\neg }\mathbf{}â\mathbf{}\mathrm{„}\mathbf{}\mathrm{¢}$-formulas:

   The $ZÃ\mathrm{¢}â\mathrm{‚}\mathrm{\neg }â\mathrm{„}\mathrm{¢}$-formulas are obtained from the $Z$-formulas by translation. The rules are the following:

   • R1 The variables $x,y,\mathrm{\dots }$ have the translation $x^{\prime },y^{\prime },\mathrm{\dots }$

   • R2 A functional symbol $f_i$ is translated by the same symbol in $H^{\prime }$.

   • R3 "=" has the identical translation "=".

   • R4 Numerals: "0" has the translation "1", since in Heyting’s system the natural number sequence starts with "1".

   • R5 Successor: has the translation seq’.

   • R6 Propositional functions: have the translation already specified.

   • R7 Universal quantification: as in $(\forall x)A$ has the translation $(\forall x^{\prime })A^{\prime }$ if $A^{\prime }$ is the translation of $A$.

   By closer scrutiny Rules 3.B and R4 turn out to be inconsistent.

   By 3.B the definition of functions by recursion is introduced and by R4 "0" has the translation "1".

   So if we consider the usual recursive definitions of $x+y$, $x-y$ or $x^y$, the first recursion equation after translation is:

   $x^{\prime }+1=x^{\prime }$

   $x^{\prime }-1=x^{\prime }$

   $x^{\prime 1}=1$

   If both rules were to be allowed we could prove the inconsistency of $H^{\prime }$.

   The informal argument is the following:

   The recursive definition of $+$, for example, gives for the first equation:

   $x+0=x.$

   The translation of this formula in $H^{\prime }$ is therefore:

   $x^{\prime }+1=x^{\prime }.$

   But by definition of successor, $x^{\prime }+1$ is the successor of $x^{\prime }$. This entails that $x^{\prime }$ is its own successor. But by axiom 10.26 no number can be its own successor, hence the contradiction.

   Here is the derivation:

   1.	$x+0=x$	First rec. eq.
   2.	$x^{\prime }+1=x^{\prime }$	1, R1, R3, R4
   3.	$x^{\prime }+1=\text{seq’}{x}^{\prime }$	$H2$, 10.03
   4.	$x^{\prime }=\text{seq’}{x}^{\prime }$	2, 3, $H2$, 10.221
   5.	$\mathrm{\neg }(x^{\prime }=\text{seq’}{x}^{\prime })$	$H2$, 10.26
   6.	$x^{\prime }=\text{seq’}{x}^{\prime }\wedge \mathrm{\neg }(x^{\prime }=\text{seq’}{x}^{\prime })$	4, 5, $H1$, 1.2

   Since we can not let go of 3.B, the moral of the story is that we have to stuff $H^{\prime }$ with a "0" and use the identical translation, as it was done with "=".

5 The main lemmas and Gödel’s translation theorem

In the following proofs we use the axioms and the theorems of Heyting 1930 divided by $H1$ (Logic) and $H2$ (Predicate calculus, Number Theory).

Actually we will be using the prime translation of those formulas together with the prime translation of the rules of inference.

Lemma 1:

If $X^{\mathrm{\prime }}$ is a $Z^{\mathrm{\prime }}$-formula, then:

$\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to X^{\prime }.$

Proof:[Complete induction on the degree of complexity of the formula.]

By definition a $Z^{\prime }$-formula is either:

• i) an atomic formula, in which case the number of connectives is 0; or

• ii) is a formula composed out of atomic formulas by means of conjunction and negation; or

• iii) is a quantified formula.

• 1. Induction basis

  Since $Z^{\prime }$ is a translation of a numerical formula $Z$, obviously $Z^{\prime }\in \mathbb{N}$. Therefore we can use tertium non datur (theorem 4.45 of $H2$) as the starting formula.

  The derivation is:

  1.	$X^{\prime }\vee \mathrm{\neg }{X}^{\prime }$
  2.	$X^{\prime }\vee \mathrm{\neg }{X}^{\prime }\to \mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to X^{\prime }$	Theor. 4.45 ($H1$)
  3.	$\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to X^{\prime }$	1, 2, MP

• 2. Inductive step

  The inductive hypothesis is that we already have proofs for X’ and Y’ in H’.

  1. First Case: Conjunction

     1.	$\mathrm{\neg }\mathrm{\neg }(X^{\prime }\wedge Y^{\prime })\to \mathrm{\neg }\mathrm{\neg }{X}^{\prime }\wedge \mathrm{\neg }\mathrm{\neg }{Y}^{\prime }$	4.61 ($H1$)
     2.	$\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\wedge \mathrm{\neg }\mathrm{\neg }{Y}^{\prime }\to X^{\prime }\wedge Y^{\prime }$	1, IB, IH
     3.	$\mathrm{\neg }\mathrm{\neg }(X^{\prime }\wedge Y^{\prime })\to X^{\prime }\wedge Y^{\prime }$	1, 2, 2.29 ($H1$)

  2. Second Case: Negation

     1.	$\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to X^{\prime }$	IH
     2.	$\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to \mathrm{\neg }{X}^{\prime }$	4.32 ($H1$)

  3. Third Case: $\forall$

     1.	$\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to X^{\prime }$	IH
     2.	$(\forall x^{\prime })\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to X^{\prime }$	1, 5.8 ($H2$)
     3.	$(\forall x^{\prime })\mathrm{\neg }\mathrm{\neg }{X}^{\prime }\to (\forall x^{\prime })X^{\prime }$	6.4 ($H2$)
     4.	$\mathrm{\neg }\mathrm{\neg }(\forall x^{\prime })X^{\prime }\to (\forall x^{\prime })\mathrm{\neg }\mathrm{\neg }{X}^{\prime }$	6.78 ($H2$)
     5.	$\mathrm{\neg }\mathrm{\neg }(\forall x^{\prime })X^{\prime }\to (\forall x^{\prime })X^{\prime }$	3, 4, 2.29 ($H1$)

Lemma 2:

If $X\mathit{}Ã\mathit{}\mathrm{¢}\mathit{}â\mathit{}\mathrm{‚}\mathit{}\mathrm{\neg }\mathit{}â\mathit{}\mathrm{„}\mathit{}\mathrm{¢}$ and $Y\mathit{}Ã\mathit{}\mathrm{¢}\mathit{}â\mathit{}\mathrm{‚}\mathit{}\mathrm{\neg }\mathit{}â\mathit{}\mathrm{„}\mathit{}\mathrm{¢}$ are $Z\mathit{}Ã\mathit{}\mathrm{¢}\mathit{}â\mathit{}\mathrm{‚}\mathit{}\mathrm{\neg }\mathit{}â\mathit{}\mathrm{„}\mathit{}\mathrm{¢}$-formulas then in $H\mathit{}Ã\mathit{}\mathrm{¢}\mathit{}â\mathit{}\mathrm{‚}\mathit{}\mathrm{\neg }\mathit{}â\mathit{}\mathrm{„}\mathit{}\mathrm{¢}$:

$X^{\prime }\to Y^{\prime }\leftrightarrow \mathrm{\neg }(XÃ\mathrm{¢}â\mathrm{‚}\mathrm{\neg }â\mathrm{„}\mathrm{¢}\wedge \mathrm{\neg }YÃ\mathrm{¢}â\mathrm{‚}\mathrm{\neg }â\mathrm{„}\mathrm{¢}).$

Proof:

1.	$X^{\prime }\to Y^{\prime }\to \mathrm{\neg }(X^{\prime }\wedge \mathrm{\neg }{Y}^{\prime })$	4.9 ($H1$)
2.	$\mathrm{\neg }(X^{\prime }\wedge \mathrm{\neg }{Y}^{\prime })\to X^{\prime }\to \mathrm{\neg }\mathrm{\neg }{Y}^{\prime }$	4.52 ($H1$)
3.	$\mathrm{\neg }(X^{\prime }\wedge \mathrm{\neg }{Y}^{\prime })\to X^{\prime }\to Y^{\prime }$	2, Lemma 1

Proposition 1: [Gödel’s Hauptsatz: The translation theorem ]

If $X$ is a provable formula in Herbrand’s system then:

its Gödel-translation is provable in $H^{\mathrm{\prime }}$.

Proof:

1. The axioms:

   • i) Group A

     Each of the Group A axioms from Herbrand’s system is equivalent to the following propositions of $H2$:

     10.2 $(p\in \mathbb{N}\to p=p)$

     10.22 $(p\in \mathbb{N}\wedge p=q\to q=p)$

     10.221 $(p\in \mathbb{N}\wedge p=q\wedge q=r\to p=r)$

     10.25 $(p\in \mathbb{N}\wedge q\in N\to (p=q)\vee \mathrm{\neg }(p=q))$

     10.26 $(p\in \mathbb{N}\to \mathrm{\neg }(\text{seq’}p=p))$

   • ii) Group B

     Herbrand’s Group B axioms have the following translation:

     $\varphi (1)\wedge (\forall x^{\prime })\varphi (x^{\prime })\to \varphi (\text{seq’}{x}^{\prime })\to (\forall x^{\prime })\varphi (x^{\prime })$

     Lemma 2 allows the substitution of both occurrences of "$\beta \to \beta$" by $\mathrm{\neg }(\alpha \wedge \mathrm{\neg }\beta ).$

     After the substitution one then gets the formula:

     $\mathrm{\neg }\varphi (1)\wedge \mathrm{\neg }[(\forall x^{\prime })\varphi (x^{\prime })\wedge \mathrm{\neg }(\text{seq’}{x}^{\prime })]\wedge \mathrm{\neg }(\forall x^{\prime })\varphi (x^{\prime }).$

     The formula is the translation of a Group B axiom and is identical with the formula 1014 from $H2$.

   • iii) Group C and Group D

     Their adjunction was already realized.

   • iv) Group E

     Follows directly from the Lemmas.

   • v) Group F

     Use Lemma 2 and from $H2$ 6.3 and 5.4.

   • vi) Group G

     Follows directly from $H2$ 6.26 and 10.01.

2. Rules of inference:

   • i) Modus ponens

     We have to prove that if $X^{\prime }$ and ${(X\to Y)}^{\prime }$ are provable in $H^{\prime }$ then $Y^{\prime }$ is also provable in $H^{\prime }$.

     Now by Lemma 2:

     ${(X\to Y)}^{\prime }\leftrightarrow \mathrm{\neg }{(X\wedge \mathrm{\neg }Y)}^{\prime }.$

     This means that ${(X\to Y)}^{\prime }$ is equivalent to:

     $\mathrm{\neg }(X^{\prime }\wedge \mathrm{\neg }{Y}^{\prime }).$

     The intuitionistic interpretation of this formula is that we can derive a contradiction from the fact that we have a proof of $X^{\prime }$ and not a proof of $Y^{\prime }$.

     Since by hypothesis $X^{\prime }$ has a proof in $H^{\prime }$, $Y^{\prime }$ is also provable by 1.3 of $H1$.

   • ii) $\forall$-Introduction in Implicatum

     The Gödel-translation is:

     $(X^{\prime }\to Y^{\prime })\to [X^{\prime }\to (\forall x^{\prime })Y^{\prime }].$

     But this is equivalent to:

     $[\mathrm{\neg }(X^{\prime }\wedge \mathrm{\neg }{Y}^{\prime })]\to [X^{\prime }\to (\forall x^{\prime })Y^{\prime }]$

     and the last formula follows by 5.5 ($H2$) and Lemma 2.

Discussion:

Gödel’s Hauptsatz shows that the set of all theorems of Herbrand’s system is a subset of the set of theorems of $H^{\prime }$.

Thus, if we assume that intuitionistic arithmetic is consistent, the Hauptsatz delivers a proof of the consistency of classical number theory, since an inconsistency in $Z$ would entail the inconsistency of $H^{\prime }$.

Gödel points out that this proof is not finitistic in Hilbert’s sense, due to the several occurrences of the abstract concepts of $H^{\prime }$ like "construction" and "proof".

This in turn entails the question, which Gödel addressed in 1941 in his Yale lecture, to determine to what extent is then intuitionistic logic itself constructive. In the PM entry "the interpretation of intuitionistic logic by means of functionals" it will be reported on Gödel’s negative answer to this question.

6 Complementary material

See "the interpretation of intuitionistic logic by means of functionals" (http://planetmath.org/InterpretationOfIntuitionisticLogicByMeansOfFunctionals). See also parent entry "intuitionistic logic" (http://planetmath.org/IntuitionisticLogic).

Title	the inclusion of classical into intuitionistic logic
Canonical name	TheInclusionOfClassicalIntoIntuitionisticLogic
Date of creation	2013-03-22 18:32:28
Last modified on	2013-03-22 18:32:28
Owner	gribskoff (21395)
Last modified by	gribskoff (21395)
Numerical id	10
Author	gribskoff (21395)
Entry type	Topic
Classification	msc 03B20
Classification	msc 03A05
Classification	msc 03-01
Synonym	Brouwer’s logic
Synonym	intuitionistic foundations
Synonym	consistency proof
Related topic	IntuitionisticLogic
Related topic	AnOutlineOfHilbertsProgramme
Related topic	FOUNDATIONSOFMATHEMATICSOVERVIEW
Related topic	Logicism
Defines	intuitionistic proof
Defines	Gödel’s translation mapping