[FOM] 708: Second Incompleteness/3
Harvey Friedman
hmflogic at gmail.com
Sun Sep 11 22:33:29 EDT 2016
Recall the outline from 707: Second Incompleteness/2 below. Here we do
3.1, 3.2, 3.3.
1. INTRODUCTION
2. INTERPRETATION THEOREMS/ARITHMETIC
3. NO INTERPRETATION THEOREMS/ARITHMETIC
3.1. OVER PA
3.2. OVER PRA
3.3. OVER SEFA
3.4. OVER EFA
3.5. OVER PFA
4. NO INTERPRETATION THEOREMS/STRINGS
5. NO INTERPRETATION THEOREMS/SETS
6. CHARACTERIZATION OF CONSISTENCY STATEMENTS
1. INTRRODUCTION
See 707: Second Incompleteness/2.
2. INTERPRETATION THEOREMS/ARITHMETIC
See 707: Second Incompleteness/2.
3. NO INTERPRETATION THEOREMS
3..1. OVER PA
Here PA = Peano Arithmetic is formulated in the language 0,S,+,x,exp,<
unless otherwise indicated. T is an extension of S if and only if the
language of T extends the language of S and the axioms of T extend the
axioms of S.
In sections 3.1 - 3.3, we work with the informal notion
natural formalizations of consistency statements in 0,S,+,x,exp,<
as 0,S,+,x,exp,< is the essentially weakest language supporting worry
free arithmetical coding.
Standard versions of arithmetic GSIT involve natural formalizations of
consistency statements in 0,S,+,x,exp,< and are thus informal. Here is
a particularly strong version.
INFORMAL GSIT OVER PA. No consistent r.e. presented theory T
interprets PA + Con(T). Here Con(T) is any natural formalization of
the consistency of T in 0,S,+,x,exp,< using the r.e. presentation of
T.
IMMEDIATE COROLLARY. No consistent r.e. presented extension T of PA
proves Con(T). Here Con(T) is any natural formalization of the
consistency of T in 0,S,+,x,exp,< using the r.e. presentation of T.
We now prove these from either of the following formal statements
1,2,3 below. We see that 3 implies 2 implies 1 is immediate. We also
see that 1 implies 2 implies 3 is straightforward but not as
immediate. We organize them this way because 1 already is enough to
straightforwardly derive Informal GSIT Over PA. However 3 is more
readily applicable.
FORMAL GSIT OVER PA/1. No consistent extension T of PA in
0,S,+,x,exp,< is interpretable in any theorem of T.
FORMAL GSIT OVER PA/2. No consistent extension T of PA is
interpretable in any theorem of T in 0,S,+,x,exp,<.
FORMAL GSIT OVER PA/3. No consistent theory T interprets any PA + phi
in 0,S,+,x,exp,<, where phi interprets T.
Equivalence proof: 3 implies 2 implies 1. Any counterexample to 1 is a
counterexample to 2, and any counterexample to 2 is a counterexample
to 3.
1 implies 2. Let T be a consistent extension of PA, T interpretable in
phi, T proves phi, phi in 0,S,+,x,exp,<. Let K be the set of all
theorems of T in 0,S,+,x,exp,<. Then K is a consistent extension of PA
in 0,S,+,x,exp,<, and K is interpretable in phi. Furthermore, phi is a
theorem of K. This contradicts 1.
2 implies 3. Let T be a consistent theory interpreting PA + phi in
0,S,x,exp,<, where phi interprets T. Let pi interpret PA + phi in T.
Then pi(phi) is provable in T. Let K be the theory of all sentences
alpha such that pi(alpha) is provable in T. Then K proves phi. Also K
is a consistent extension of PA in 0,S,+,x,exp,<. Furthermore, K is
interpretable in phi. This contradicts 1. By 2 implies 1, this
contradicts 2. QED
FORMAL GSIT OVER PA/4? The following is false. No consistent extension
T of PA is interpretable in any theorem of T.
Proof: Let T be EFA together with a truth predicate for sentences in
0,+,x,exp,< using goedel numberings, with the usual truth conditions,
and with the axiom that every sentence of PA is true. Then T is a
consistent extension of PA, and since T is finitely axiomatized, its
conjunction is a theorem in which it is interpretable. QED
We name these Formal GSIT Over PA because they so readily implies
Informal GIST Over PA by leveraging a key properties of natural
formalization of consistency statements in 0,S,+,x,exp,< - that they
support Goedel's Completeness Theorem and are true if the system is in
fact consistent. In section 6, we will carefully address properties of
consistency statements. In the present context, this is manifested by
THEOREM 2.4. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in 0,S,+,x,exp,<. There is an
interpretation of T in PA_2 + Con(T).
We now derive Informal GSIT Over PA from Formal GSIT Over PA/1.
Proof: Let T be a consistent r.e. presented theory interpreting PRA +
Con(T). By Theorem 2.4, T is interpretable in PA_2 + Con(T). Thus PA +
Con(T) is interpretable in T is interpretable in PA_2 + Con(T). Since
Con(T) is true, PA + Con(T) is consistent. Also PA_2 + Con(T) is a
theorem of PA + Con(T) by taking its conjunction (PA_2 is finitely
axiomatized). We have now violated Formal GSIT Over PA/1. QED
It remains to prove Formal GSIT Over PA/1.
Proof: Let T be a consistent extension of PA in 0,S,+,x,exp,<.. Let T
be interpretable in alpha, where T proves alpha. Let K be PA together
with finitely many axioms of T, such that K proves alpha. Clearly K is
a consistent extension of PA and K is interpretable in alpha.
Clearly PA + Con(alpha) proves Con(K). This is because K is
interpretable in alpha and the language of K is finite, and so any
interpretation of K in alpha can be formally verified in PA. Hence PA
+ Con(alpha) proves Con(PA + alpha). We claim that PA + alpha proves
Con(alpha). This is proved by cut elimination for first order
predicate calculus with equality (available in PA) and inductions on a
truth predicate for subformulas of alpha, as is well known.
Hence PA + Con(alpha) proves Con(PA + Con(alpha)), since we can
replace the inside PA + alpha with PA + Con(alpha). Hence by GSIT, PA
+ Con(alpha) is inconsistent. Hence PA + alpha is inconsistent.
Therefore K is inconsistent. This is a contradiction. QED
3.2. OVER PRA
PRA = primitive recursive arithmetic, which is in the language prim =
0,S,<,.., with all of the primitive recursive function symbols. Recall
EFA = exponential function arithmetic in 0,S,+,x,exp,< used in section
2.
Let sigma be a fragment of prim. Our familiar 0,S,+,x,exp,< is a
fragment of prim. Pi01(sigma) is the set of all sentences in sigma
that begin with zero or more universal quantifiers followed by a
bounded formula. Note that PRA(prim) is Pi01(prim) - i.e., a set of
Pi01(prim) sentences.
As we are working over PRA with prim, we can conveniently consider
natural formalizations of consistency in prim. We need to make a move
that we did not make in section 3.1. Namely, that we consider all
natural formalizations of the consistency of T in prim to be
Pi01(prim).
INFORMAL GSIT OVER PRA. No consistent r.e. presented theory T
interprets PRA + Con(T). Here Con(T) is any natural formalization of
the consistency of T in Pi01(prim) using the r.e. presentation of T.
IMMEDIATE COROLLARY. No consistent r.e. presented extension T of PRA
proves Con(T). Here Con(T) is any natural formalization of the
consistency of T in PI01(prim) using the r.e. presentation of T.
We now prove these from either of the following formal statements
1,2,3 below. We see that 3 implies 2 implies 1 is immediate. We also
see that 1 implies 2 implies 3 is straightforward but not as
immediate. We organize them this way because 1 already is enough to
straightforwardly derive Informal GSIT Over PRA. However 3 is more
readily applicable.
FORMAL GSIT OVER PRA/1. No consistent extension T of PRA in prim is
interpretable in any Pi01(prim) theorem of T.
FORMAL GSIT OVER PRA/2. No consistent extension T of PRA is
interpretable in any Pi01(prim) theorem of T.
FORMAL GSIT OVER PRA/3. No consistent theory T interprets any PRA +
phi in Pi01(prim), where phi interprets T.
Equivalence proof: 3 implies 2 implies 1. Any counterexample to 1 is a
counterexample to 2, and any counterexample to 2 is a counterexample
to 3.
1 implies 2. Let T be a consistent extension of PRA, T interpretable
in phi, T proves phi, phi in prim. Let K be the set of all theorems of
T in prim. Then K is a consistent extension of PRA in prim, and K is
interpretable in phi. Furthermore, phi is a theorem of K. This
contradicts 1.
2 implies 3. Let T be a consistent theory interpreting PRA + phi in
prim, where phi interprets T. Let pi interpret PRA + phi in T. Then
pi(phi) is provable in T. Let K be the theory of all sentences alpha
such that pi(alpha) is provable in T. Then K proves phi. Also K is a
consistent extension of PRA in prim. Furthermore, K is interpretable
in phi. This contradicts 1. By 2 implies 1, this contradicts 2. QED
FORMAL GSIT OVER PRA/4? The following is false. No consistent
extension T of PRA in prim is interpretable in any theorem of T.
Proof: Let T be PRA together with phi = "the natural Turing machine
set up to compute the Ackerman function terminates at all inputs",
where phi is in 0,S,+,x,exp,<. Then PRA is interpretable in EFA + phi,
and EFA + phi (taking its conjunction) is a theorem of T. QED
We now use the following from section 2.
THEOREM 2.5. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in 0,S,+,x,exp,<. There is an
interpretation of T in EFA + Con(T).
For this section, it is convenient to use the following modification
with same (or slightly easier) proof.
THEOREM 2.5'. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in prim. There is an
interpretation of T in a finite fragment of PRA + Con(T).
We now derive Informal GSIT Over PRA from Formal GSIT Over PRA/1.
Proof: Let T be a consistent r.e. presented theory interpreting PRA +
Con(T). By Theorem 2.5', T is interpretable in a finite fragment of K
of PRA + Con(T). Thus PRA + Con(T) is interpretable in T is
interpretable in K. Since Con(T) is true, PRA + Con(T) is consistent.
Also K is a theorem of PRA + Con(T), and K is Pi01(prim), as a
conjunction. We have now violated Formal GSIT Over PA/1. QED
It remains to prove Formal GSIT Over PA/1.
Proof: Let T be a consistent extension of PRA in prim. Let T be
interpretable in alpha, where T proves alpha, and alpha is Pi01(prim).
Let K be PA together with finitely many axioms of T, such that K
proves alpha. Clearly K is a consistent extension of PA and K is
interpretable in alpha.
Clearly PA + Con(alpha) proves Con(K). This is because K is
interpretable in alpha and the language of K is finite, and so any
interpretation of K in alpha can be formally verified in PA. Hence PA
+ Con(alpha) proves Con(PA + alpha). We claim that PA + alpha proves
Con(alpha). This is proved by cut elimination for first order
predicate calculus with equality (available in PA) and inductions on a
truth predicate for subformulas of alpha, as is well known.
Hence PA + Con(alpha) proves Con(PA + Con(alpha)), since we can
replace the inside PA + alpha with PA + Con(alpha). Hence by GSIT, PA
+ Con(alpha) is inconsistent. Hence PA + alpha is inconsistent.
Therefore K is inconsistent. This is a contradiction. QED
3.3. OVER SEFA.
SEFA = superexponential function arithmetic, is in the language
0,S,+.x.exp,superexp,<, and is finitely axiomatized.
INFORMAL GSIT OVER SEFA. No consistent r.e. presented theory T
interprets SEFA + Con(T). Here Con(T) is any natural formalization of
the consistency of T in 0,S,+,x,exp,< using the r.e. presentation of
T.
IMMEDIATE COROLLARY. No consistent r.e. presented extension T of SEFA
proves Con(T). Here Con(T) is any natural formalization of the
consistency of T in 0,S,+,x,exp,< using the r.e. presentation of T.
We now prove these from either of the following formal statements
1,2,3 below. We see that 3 implies 2 implies 1 is immediate. We also
see that 1 implies 2 implies 3 is straightforward but not as
immediate. We organize them this way because 1 already is enough to
straightforwardly derive Informal GSIT Over PA. However 3 is more
readily applicable.
FORMAL GSIT OVER SEFA/1. No consistent extension T of SEFA in
0,S,+,x,expsuperexp,< is interpretable in any Pi01(0,S,+,exp,<)
theorem of T.
FORMAL GSIT OVER SEFA/2. No consistent extension T of SEFA is
interpretable in any Pi01(0,S,+,exp,<) theorem of T.
FORMAL GSIT OVER SEFA/3. No consistent theory T interprets any SEFA +
phi, phi in Pi01(0,S,+,x,exp,<), where phi interprets T.
Equivalence proof: 3 implies 2 implies 1. Any counterexample to 1 is a
counterexample to 2, and any counterexample to 2 is a counterexample
to 3.
1 implies 2. Let T be a consistent extension of SEFA, T interpretable
in phi, T proves phi, phi in Pi01(0,S,+,x,exp,<). Let K be the set of
all theorems of T in 0,S,+,x,exp,<. Then K is a consistent extension
of SEFA in 0,S,+,x,exp,<, and K is interpretable in phi. Furthermore,
phi is a theorem of K. This contradicts 1.
2 implies 3. Let T be a consistent theory interpreting SEFA + phi, phi
in Pi01(0,S,x,exp,<), where phi interprets T. Let pi interpret SEFA +
phi in T. Then pi(phi) is provable in T. Let K be the theory of all
sentences alpha such that pi(alpha) is provable in T and alpha in
Pi01(0,S,+,x,exp,<). Then K proves phi. Also K is a consistent
extension of SEFA in 0,S,+,x,exp,<. Furthermore, K is interpretable in
phi. This contradicts 1. By 2 implies 1, this contradicts 2. QED
FORMAL GSIT OVER PA/4? The following is false. No consistent extension
T of SEFA is interpretable in any theorem of T.
Proof: Let T be SEFA together with phi = "all of the natural Turing
machines set up to compute the super exponential terminates at all
inputs", where phi is in 0,S,+,x,exp,<. Then SEFA is interpretable in
EFA + phi, and EFA + phi (taking its conjunction) is a theorem of T.
QED
We name these Formal GSIT Over SEFA because they so readily implies
Informal GIST Over SEFA by leveraging a key properties of natural
formalization of consistency statements in 0,S,+,x,exp,< - that they
support Goedel's Completeness Theorem and are true if the system is in
fact consistent. In section 6, we will carefully address properties of
consistency statements. In the present context, this is manifested by
THEOREM 2.5. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in 0,S,+,x,exp,<. There is an
interpretation of T in EFA + Con(T).
We now derive Informal GSIT Over SEFA from Formal GSIT Over SEFA/1.
Proof: Let T be a consistent r.e. presented theory interpreting SEFA +
Con(T). By Theorem 2.5, T is interpretable in EFA + Con(T). Thus SEFA
+ Con(T) is interpretable in T is interpretable in EFA + Con(T). Since
Con(T) is true, SEFA + Con(T) is consistent. Also EFA + Con(T) is a
theorem of SEFA + Con(T) by taking its conjunction (EFA is finitely
axiomatized). We have now violated Formal GSIT Over SEFA/1. QED
It remains to prove Formal GSIT Over SEFA/1.
Proof: Let T be a consistent extension of SEFA in
0,S,+,x,exp,superexp,<. Let T be interpretable in alpha, where T
proves alpha and alpha is Pi01(0,S,+,x,exp,<). Let K be SEFA together
with finitely many axioms of T, such that K proves alpha. Clearly K is
a consistent extension of SEFA and K is interpretable in alpha.
Clearly SEFA + Con(alpha) proves Con(K). This is because K is
interpretable in alpha and the language of K is finite, and so any
interpretation of K in alpha can be formally verified in SEFA. Hence
SEFA + Con(alpha) proves Con(PA + alpha). We claim that SEFA + alpha
proves Con(alpha). This is proved by cut elimination for first order
predicate calculus with equality (available in SEFA) and inductions on
a truth predicate for subformulas of alpha, as is well known.
Hence SEFA + Con(alpha) proves Con(SEFA + Con(alpha)), since we can
replace the inside SEFA + alpha with PA + Con(alpha). Hence by GSIT,
SEFA + Con(alpha) is inconsistent. Hence SEFA + alpha is inconsistent.
Therefore K is inconsistent. This is a contradiction. QED
***********************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 708th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-699 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
Harvey Friedman
More information about the FOM
mailing list