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.
Contents:
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 truthfunctions 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.
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$.
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.
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. ${(\mathcal{X}\wedge \mathcal{Y})}^{\prime}\leftrightarrow {\mathcal{X}}^{\prime}\wedge {\mathcal{Y}}^{\prime}$
B. ${(\mathcal{X}\vee \mathcal{Y})}^{\prime}\leftrightarrow \mathrm{\neg}(\mathrm{\neg}{\mathcal{X}}^{\prime}\wedge \mathrm{\neg}{\mathcal{Y}}^{\prime})$
C. ${(\mathcal{X}\to \mathcal{Y})}^{\prime}\leftrightarrow \mathrm{\neg}({\mathcal{X}}^{\prime}\wedge \mathrm{\neg}{\mathcal{Y}}^{\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.
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 validitypreserving 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{}\xc3\mathbf{}\mathrm{\xa2}\mathbf{}\xe2\mathbf{}\mathrm{\x82}\mathbf{}\mathrm{\neg}\mathbf{}\xe2\mathbf{}\mathrm{\x84}\mathbf{}\mathrm{\xa2}$formulas:
The $Z\xc3\mathrm{\xa2}\xe2\mathrm{\x82}\mathrm{\neg}\xe2\mathrm{\x84}\mathrm{\xa2}$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$, $xy$ 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\u2019}{x}^{\prime}$ $H2$, 10.03 4. ${x}^{\prime}=\text{seq\u2019}{x}^{\prime}$ 2, 3, $H2$, 10.221 5. $\mathrm{\neg}({x}^{\prime}=\text{seq\u2019}{x}^{\prime})$ $H2$, 10.26 6. ${x}^{\prime}=\text{seq\u2019}{x}^{\prime}\wedge \mathrm{\neg}({x}^{\prime}=\text{seq\u2019}{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’.

(a)
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$) 
(b)
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$) 
(c)
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$)

(a)
Lemma 2:
If $X\mathit{}\xc3\mathit{}\mathrm{\xa2}\mathit{}\xe2\mathit{}\mathrm{\x82}\mathit{}\mathrm{\neg}\mathit{}\xe2\mathit{}\mathrm{\x84}\mathit{}\mathrm{\xa2}$ and $Y\mathit{}\xc3\mathit{}\mathrm{\xa2}\mathit{}\xe2\mathit{}\mathrm{\x82}\mathit{}\mathrm{\neg}\mathit{}\xe2\mathit{}\mathrm{\x84}\mathit{}\mathrm{\xa2}$ are $Z\mathit{}\xc3\mathit{}\mathrm{\xa2}\mathit{}\xe2\mathit{}\mathrm{\x82}\mathit{}\mathrm{\neg}\mathit{}\xe2\mathit{}\mathrm{\x84}\mathit{}\mathrm{\xa2}$formulas then in $H\mathit{}\xc3\mathit{}\mathrm{\xa2}\mathit{}\xe2\mathit{}\mathrm{\x82}\mathit{}\mathrm{\neg}\mathit{}\xe2\mathit{}\mathrm{\x84}\mathit{}\mathrm{\xa2}$:
${X}^{\prime}\to {Y}^{\prime}\leftrightarrow \mathrm{\neg}(X\xc3\mathrm{\xa2}\xe2\mathrm{\x82}\mathrm{\neg}\xe2\mathrm{\x84}\mathrm{\xa2}\wedge \mathrm{\neg}Y\xc3\mathrm{\xa2}\xe2\mathrm{\x82}\mathrm{\neg}\xe2\mathrm{\x84}\mathrm{\xa2}).$
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ödeltranslation 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\u2019}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\u2019}{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\u2019}{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ödeltranslation 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).
References
 1 Brouwer, L., Collected works: vol. 1, North Holland, Amsterdam, 1975.
 2 Brouwer, L., "Mathematik, Wissenschaft und Sprache", Monatshefte fÃÂ¼r Mathematik und Physik, Leipzig, 1929.
 3 Brouwer, L., "Consciousness, philosophy and mathematics", ed. W. Beth, Library of the tenth international congress of philosophy, Amsterdam, 1948.
 4 Dummett, M., Elements of intuitionism, Clarendon Press, Oxford, 1977.
 5 Gödel, K., Collected works, ed. S. Feferman, Oxford, 19872003.
 6 Heyting, A. Intuitionism: An introduction, 3. ed., NorthHolland, Amsterdam, 1971.
 7 Hilbert, D., and, Ackermann, GrundzÃÂ¼ge der theoretischen Logik, Berlin, 1949.
 8 Kleene, S., Introduction to metamathematics^{}, NorthHolland, Amsterdam, 1964.
 9 Rasiowa, H., and, Sikorski, R., The mathematics of metamathematics, Warsaw, 1963.
 10 Tarski, A., "Der AussagenkalkÃÂ¼l und die Topologie", Fundamenta Mathematicae, 31, 1938.
Title  the inclusion of classical into intuitionistic logic 
Canonical name  TheInclusionOfClassicalIntoIntuitionisticLogic 
Date of creation  20130322 18:32:28 
Last modified on  20130322 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 0301 
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 