the inclusion of classical into intuitionistic logic
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.
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
A. Classical propositional calculus ():
"", "", ""
B. Intuitionistic propositional calculus ():
denote the intuitionistic connectives negation and conjunction, respectively.
Let be a well formed formula of which consists only of conjunctions and negations. If is valid in then it is demonstrable in .
This means that must have the form:
If the formula is valid in then each is also valid. Glivenko proves that is provable in , as we can see in Heyting (1930), pg. 43.
In that case the whole formula is also provable in .
The generalized Glivenko’s theorem
To see this one translates a classically valid formula into a formula of . The translations rules are the following:
A. Negation: the classical function has the translation ;
B. Disjunction: the classical function has the translation:
C. Implication: the classical function has the translation:
D. Conjunction: the classical function has the translation:
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:
A. The functions of the classical propositional calculus
B. Numerical variables: small Roman , ,
C. Universal quantifiers: , ,
D. Equality: "="
E. Numerals: 0, 1,
To each symbol one associates an integer , which denotes the number of arguments of .
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 is a numerical expression is a numerical expression;
iii) If , , are numerical expressions then:
is a numerical expression.
An atomic formula is an equality, the terms of which are numerical expressions. Thus:
is an atomic formula.
i) An atomic formula is a -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 -formulas.
A. Herbrand’s axioms in particular from to .
Three axioms are introduced with the following content:
Axiom E: [Rule of insertion]
Every numerical expression that results from the insertion of a -formula in a tautology of the propositional calculus is an axiom.
Axiom F: [Dictum de omni]
If is a -formula and is a numerical expression such that the variables of are not bound in , then all formulas of the pattern:
Axiom G: [Leibniz]
If is a -formula then all formulas of the pattern:
A. Modus ponens
From and we are allowed to infer .
B. -Introduction in the implicatum
If does not occur free in then from we are allowed to infer .
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 , , are not numerical variables; they rather denote objects.
The translation mapping "":
If are object variables from Heyting’s system, they will be translated into numerical variables by means of Gödel’s translation mapping "" as being now variables for natural numbers.
The notation is defined by the rules:
D. If is a formula in which these variables occur free then:
E. If is a formula then:
The relevant formulas belong to [of , on the basic definitions and inference rules] and [of , 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 "" by "".
i) For a propositional variable any expression can be inserted and
ii) For an object variable a symbolic expression can be inserted, if 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:
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 allow the introduction of functions such that the computation of is always possible for any -tuple of numbers.
Ex.: if a function has already been introduced then we can define a new function by recursion on with the following recursion equations:
The axioms of Group and the axioms of Group , which allow the introduction of universal quantifiers, are adjoined to . The resulting system will be called .
The -formulas are obtained from the -formulas by translation. The rules are the following:
R1 The variables have the translation
R2 A functional symbol is translated by the same symbol in .
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 has the translation if is the translation of .
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 , or , the first recursion equation after translation is:
If both rules were to be allowed we could prove the inconsistency of .
The informal argument is the following:
The recursive definition of , for example, gives for the first equation:
The translation of this formula in is therefore:
But by definition of successor, is the successor of . This entails that is its own successor. But by axiom 10.26 no number can be its own successor, hence the contradiction.
Here is the derivation:
1. First rec. eq. 2. 1, R1, R3, R4 3. , 10.03 4. 2, 3, , 10.221 5. , 10.26 6. 4, 5, , 1.2
Since we can not let go of 3.B, the moral of the story is that we have to stuff 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 (Logic) and (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.
If is a -formula, then:
By definition a -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 is a translation of a numerical formula , obviously . Therefore we can use tertium non datur (theorem 4.45 of ) as the starting formula.
The derivation is:
1. 2. Theor. 4.45 () 3. 1, 2, MP
2. Inductive step
The inductive hypothesis is that we already have proofs for X’ and Y’ in H’.
First Case: Conjunction
1. 4.61 () 2. 1, IB, IH 3. 1, 2, 2.29 ()
Second Case: Negation
1. IH 2. 4.32 ()
1. IH 2. 1, 5.8 () 3. 6.4 () 4. 6.78 () 5. 3, 4, 2.29 ()
If and are -formulas then in :
1. 4.9 () 2. 4.52 () 3. 2, Lemma 1
Proposition 1: [Gödel’s Hauptsatz: The translation theorem ]
If is a provable formula in Herbrand’s system then:
its Gödel-translation is provable in .
i) Group A
Each of the Group A axioms from Herbrand’s system is equivalent to the following propositions of :
ii) Group B
Herbrand’s Group B axioms have the following translation:
Lemma 2 allows the substitution of both occurrences of "" by
After the substitution one then gets the formula:
The formula is the translation of a Group B axiom and is identical with the formula 1014 from .
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 6.3 and 5.4.
vi) Group G
Follows directly from 6.26 and 10.01.
Rules of inference:
i) Modus ponens
We have to prove that if and are provable in then is also provable in .
Now by Lemma 2:
This means that is equivalent to:
The intuitionistic interpretation of this formula is that we can derive a contradiction from the fact that we have a proof of and not a proof of .
Since by hypothesis has a proof in , is also provable by 1.3 of .
ii) -Introduction in Implicatum
The Gödel-translation is:
But this is equivalent to:
and the last formula follows by 5.5 () and Lemma 2.
Gödel’s Hauptsatz shows that the set of all theorems of Herbrand’s system is a subset of the set of theorems of .
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 would entail the inconsistency of .
Gödel points out that this proof is not finitistic in Hilbert’s sense, due to the several occurrences of the abstract concepts of 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).
- 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, 1987-2003.
- 6 Heyting, A. Intuitionism: An introduction, 3. ed., North-Holland, Amsterdam, 1971.
- 7 Hilbert, D., and, Ackermann, GrundzÃÂ¼ge der theoretischen Logik, Berlin, 1949.
- 8 Kleene, S., Introduction to metamathematics, North-Holland, 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|
|Date of creation||2013-03-22 18:32:28|
|Last modified on||2013-03-22 18:32:28|
|Last modified by||gribskoff (21395)|
|Defines||Gödel’s translation mapping|