[FOM] 707: Second Incompleteness/2

[Harvey Friedman]

Here we continue from
http://www.cs.nyu.edu/pipermail/fom/2016-September/020060.html where
we had an initial version of section 1, and section 2 just for PA. In
this posting we will add to section 2 for EFA. In the next posting, we
will present much of section 3. To complete section 3 later, we plan
to add to section 2 again, for PFA.

SECOND INCOMPLETENESS

ABSTRACT. We show that, in various senses and environments, if a
formalization of consistency statements supports the Goedel
Completeness Theorem, then it supports the Goedel Second
Incompleteness Theorem. This is preceded by No Interpretation Theorems
that directly imply standard formulations of Goedel's Second
Incompleteness Theorem.

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. INTRODUCTION

As in http://www.cs.nyu.edu/pipermail/fom/2016-September/020060.html

2. INTERPRETATION THEOREMS

Same as in http://www.cs.nyu.edu/pipermail/fom/2016-September/020060.html
until here.

LEMMA 2.1. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in PA. There is a
definition in L(PA) that, provably in PA + Con(T), defines a complete
diagrammatic model of T. Here T is referred to, in PA, via its r.e.
presentation.

Proof: Same as in
http://www.cs.nyu.edu/pipermail/fom/2016-September/020060.html We
correct a typo. {rho_0,...,rho_n-1,psi_n} should be
{rho_0,...,rho_3n,psi_n}.

Same as in http://www.cs.nyu.edu/pipermail/fom/2016-September/020060.html
until here.

LEMMA 2.2. Let T be an r.e. presented theory. Let W be an extension of
PA in L(PA). Suppose there is a definition in L(PA) that, provably in
W, defines a complete diagrammatic model M of T. Here T is referred
to, in PA, via its r.e. presentation. Then there is an interpretation
of T in W.

Proof: Same as in
http://www.cs.nyu.edu/pipermail/fom/2016-September/020060.html until
here.

THEOREM 2.3. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in PA. There is an
interpretation of T in PA + Con(T).

Proof: Immediate from Lemmas 2.1 and 2.2. QED

We first move PA down a lot without changing the proof of Theorem 2.3
before we move PA down all the way to EFA = exponential function
arithmetic, where we really have to be much more careful and use cuts.

PA_n, n >= 1, is PA with induction only for Sigma0n formulas. This is
also known as ISigma_n. These are the formulas beginning with at most
n alternating blocks of quantifiers starting with zero or more
existential quantifiers, followed by a bounded formula. It is well
known that we can require that all blocks have length 1, and also omit
the requirement that we start with an existential quantifier, and
obtain a logically equivalent theory.

THEOREM 2.4. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in PA_2. There is an
interpretation of T in PA_2 + Con(T).

Proof: The key point is that PA_2 suffices to construct
rho_0,rho_1,..., and the various constructions are internally in class
delta02. QED

We now move PA way down to EFA = exponential function arithmetic, also
known as ISigma_0(exp) in the language 0,S,+,x,exp,<. Lemma 2.1 has to
be modified as we are not going to be able to prove Lemma 2.1 with PA
replaced throughout by EFA. We only get what amounts to a complete
diagrammatic model of T along a cut, which is weaker., but good enough
to interpret T. Here a cut is a defined nonempty set of nonnegative
integers, closed downward, without a greatest element. There is the
trivial cut consisting of all nonnegative integers. However, any
failure of induction defines a bounded cut. Of course, according to
PA, there are no bounded cuts.

THEOREM 2.5. Let T be an r.e. presented theory, and Con(T) be any
natural formalization of the consistency of T in EFA. There is an
interpretation of T in EFA + Con(T).

Proof: We work in EFA + Con(T). After a certain development, we then
take any model M of EFA + Con(T) and appropriately M define a model of
T.

Let TM be the set of all terms, AF the set of all atomic formulas, FM
the set of all formulas, in FOL(=) with special constants d_0,d_1,...
added. We need to build a hierarchy for TM, AF, FM with some care in a
way that is supported by EFA. Recall that variables and constant
symbols have one index, where relation and function symbols have two
indices.

TM(n), n >= 0, consists of TM(n-1) together with
i. All variables v_i, i <= n.
ii. All terms F(t_1,...,t_k), where the indices of F are <= n, and
t_1,...,t_k are in TM(n-1).
iii. All terms resulting from replacing any variable v_i, i < n, by
any term in TM(n-1), in any term in TM(n-1).
iv. All d_i where 0 <= i <= 2|FM(n-1)|.

AF(n) consists of
i. All s = t, s,t in TM(n).
ii. All R(t_1,...,t_k), where the indices of R are <= n, and
t_1,...,t_k in TM(n).

FM(n), n >= 0, consists of all FM(n-1) together with
i. AF(n).
ii. All negations, binary disjunctions, binary conjunctions,
implications, and biconditionals of elements of FM(n-1).
iii. All (therexists v_i)(phi), (forall v_i)(phi), 0 <= i <= n, phi in
FM(n-1).
iv. The result of replacing any variable v_i, i < n, by any term in
TM(n), in any formula in FM(n-1).

Here we take TM(-1) = AF(-1) = FM(-1) = emptyset. The curious clause
iv for TM(n) is used to support the Henkin like construction as we
need different constants d_i for the different existential formulas
that need to be witnessed. TM, AF, FM to be. respectively, the union
over n of TM(n), AF(n), FM(n).

The purpose of FM(n) is to lay out predicate calculus so that we can
make the usual Henkin construction as in Lemma 2.1, even without
having the induction to support it. This required induction is PA_2 in
theorem 2.4. I.e., we want to end up with a Henkin like construction
even if the hierarchy FM(n) is along a bounded cut, rather than all of
the nonnegative integers.

To see that EFA supports the construction of TM(n), AF(n), FM(n), we
need to make a calculation. Suppose we know that the indices used, the
length of elements (number of symbols), and the cardinalities of
TM(n), AF(n), FM(n) are at most t > n. We want an upper bond on these
for TM(n+1), AF(n+1), FM(n+1).

The indices used in TM(n+1), AF(n+1), FM(n+1) are obviously at most
3t, The lengths of elements and the cardinalities for TM(n+1),
AF(n+1), FM(n+1)| are at most t to a reasonable power involving only
n. Hence we see that the indices used and the lengths of elements of
FM(n) is at most a double exponential in n.

Let L be the language of T together with infinitely many new constants
d_,0,d_1,..., of ten called Henkin constants. Since T is consistent in
FOL, T is also consistent in in L.

Note that the terms, atomic formulas, and formulas of L form subsets
of TM, AF, and FM. Accordingly, we define LTM(n), LAF(n), LFM(n) from
TM(n), AF(n), FM(n) by merely restricting to all elements such that
every constant, relation, and function symbol appearing has been
generated by the first n stages in the language part of the r.e.
presented theory T.

We now attempt to define finite subsets A_0,A_1,... of
LFM(0),LFM(1),... as follows.

*) Let n >= 0. List the sentences in LFM(n) in lexicographic order,
phi_0,...,phi_m. Construct +-phi_0,+-phi_1,..., +-ph_m, where for each
0 <= i <= m, we use phi_i if T U A_n-1 U
{+-phi_0,...,+-phi_i-1,phi_i} is consistent; -phi_i otherwise. Also
let psi_0,...,psi_r be the listing in lexicographic order, of the
sentences in A_n-1 that begin with an existential quantifier. Let s be
largest such that d_s appears in A_n-1. Let rho_0,...,rho_r be the
result of replacing the beginning existential quantifier in
psi_0,...,psi_r, respectively, by d_s+1,...,d_s+r. Take A_n = A_n-1 U
{+-phi_0,...,+-phi_m} U {rho_0,...,rho_r}.       T

EFA does not have near enough induction to construct the infinite
sequence A_0,A_1,... . As in the proof of Theorem 2.5, this needs
PA_2. We can of course try for a cut C where we can construct the A_i,
i in C. Even this is a problem. This is because the induction step
from A_i to A_i+1, has difficulties.

Let X be the set of all t in N, there is a unique code of a length t+1
sequence of finite subsets of FM, A_0,...,A_t, such that *) holds for
all 0 <= n <= t.

case 1. X is N.

case 2. X forms a bounded cut.

case 3. X has a greatest element t.

In case 3, what went wrong? The first part of the *) construction for
n = t+1 failed. It can be naturally set up to be a Sigma02 induction
along m there, which is bounded by a double exponential in t. This
gives us a cut below m, which by well known methods we convert to a
cut in t.

Thus in any case, we have a cut C contained in X. We try to use this
to construct a model of T. However, some more issues arise. For any
cut C containedin X, we let A(C) be the union of the A_i, i in C.

Specifically, let M be a model of the theory we are working in, EFA +
Con(T). We would like to simply take the domain of the internal model
M* of T that we are trying to construct to consist of the d_i that
appear in C. The problem is that we are required that M* interpret =
as identity. So for the domain, we instead take the set of all d_i
appearing in A(C) such that for no d_j, j < i, do we have d_i = d_j in
A(C). Note that for all d_i appearing in A(C), there is a least j such
that d_i = d_j lies in A(C). This is because membership of d_i = d_j
in A(C), j < i, is determined already in A_i.

Let M be a model of EFA + Con(T). We have already defined C, the A_i,
i in C, and A(C) within M. The clearest way to proceed to is to define
a structure M* internally in M whose language is substantially richer
than L(T), and then reduce the structure to the language L(T) to give
us the required model of T. In particular, the language of M*, L(M*),
is the portion of L(T) that is generated by the r.e. presentation of
L(T) through the stages in C, together with all of the d_i that appear
in A(C)/. It is possible that some d_i appear in A(C) without i being
in C.

As indicated above, the domain of M* will be the d_i appearing in A(C)
such that for no d_j, j < i, do we have d_i = d_j in A(C).

The interpretation any c_i from L(M*) in M* is the unique d_j in
dom(M*) such that c_i = d_j lies in A(C). Also, the interpretation of
any d_i from L(M*) is the unique d_j in dom(M*) such that d_i = d_j
lies in A(C). Here the unique d_j exists since by construction of the
A's, there exists some r with c_i = d_r (or d_i = d_r) in A(C).

The interpretation of any Rij from L(M*) in M* is given by
R*(d_a1,...,d_aij) iff Rij(d_a1,...,d_aj) in A(C), where d_a1,...,d_aj
in dom(M*).

The interpretation of any Fij from L(M*) in M* is given by
F*(d_a1,...,d_aj) is the unique d_r in dom(M*) such that
F*(d_a1,...,d_aj) = d_r lies in A(C), where d_a1,...,d_aj in dom(M*).
Note that there must be such a unique d_r in dom(M*).

We now want to show, roughly speaking, that any "formula" holds at an
assignment if and only if the sentence obtained by replacing the free
variables by their assigned elements lies in A(C). However, we do not
even have a satisfaction relation for M* as that would require more
induction than is available. So there are three approaches from here.
One is to again shorten C to accommodate the lack of induction here.
Second is to consider the desired satisfaction relation for M* to be
defined according to what we are wanting it to be. The third approach
is to simply rely on the satisfaction relation we already have
EXTERNALLY, for the part of M* whose language L', consisting of the
actual L(T) together with the d_i in L*(T). The third approach is by
far the most convenient, and the desired result needs almost no
further argumentation. Here we think of L' as the standard part of
L*(T) but with ALL of the d_i in L*(T).

We have to look at val(M*,t,alpha), where t is a term in L' and alpha
is an assignment of the variables in t from dom(M*). We need to know
that val(M*,t,alpha) = val(M*,t'), where t' is the closed term
obtained by substituting the variables in t by alpha. This is clear if
t is a variable, or a constant symbol. The external induction argument
on t is clear.

We also claim that for closed terms t in L', val(M*,t) is the unique
d_i in dom(M*) such that t = d_i lies in A(C). This is immediate if t
is a constant in L'. The external induction argument is also obvious.

Now we claim that sat(M*,s = t,alpha) iff (s = t)(alpha) lies in A(C).
Here alpha is an assignment of elements of dom(M*) to the variables in
the terms s,t in L', and  (s = t)(alpha) is the result of making the
substitution to obtain a sentence in L'. By the above, we have
sat(M*,s = t,alpha) iff val(M*,s(alpha)) = val(M*,t(alpha)). It
remains to show that val(M*,s(alpha)) = val(M*,t(alpha)) if and only
if s(alpha) = t(alpha) lies in A(C). Write val(M*,s(alpha)) = d_i,
val(M*,t(alpha)) = d_j, d_i,d_j in dom(M*), and s(alpha) = d_i,
t(alpha) = d_j lie in A(C). Then val(M*,s(alpha)) = val(M*,t(alpha))
iff d_i = d_j. Now d_i = d_j implies i = j and therefore s(alpha) =
t(alpha) lies in A(C). On the other hand, if s(alpha) = t(alpha) lies
in A(C) then d_i = d_j lies in A(C), and therefore i = j and
val(M*,s(alpha)) = val(M*,t(alpha)).

Now suppose sat(M*,phi,alpha) iff phi(alpha) in A(C), sat(M*,psi,beta)
iff psi(beta) in A(C), for any choice of assignments alpha,beta for
phi,psi, from dom(M*). Then we immediately obtain the same for
not(phi), phi and psi, phi or psi, phi implies psi, phi iff psi.

We claim sat(M*,(therexists v_i)(phi),alpha) iff (therexists
v_i)(phi)(alpha) in A(C). First suppose sat(M*,(therexists
v_i)(phi),alpha). Let d_j in dom(M*), where sat(M*,phi,alpha(v_i|d_j).
By the external induction hypothesis, phi(alpha)(alpha(v_i|d_j) lies
in A(C). Then obviously we can put the existential quantifier back
within A(C). Now suppose (therexists v_i)(phi)(alpha) lies in A(C).
Let d_j witness this in A(C). We can arrange that d_j in dom(M*).
I.e., phi(alpha(v_i|d_j) lies in A(C). By the external induction
hypothesis, sat(M*,phi,alpha(v_i|d_j)). Hence sat(M*,(therexists
v_i)(phi),alpha) as required. 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 707th 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

Harvey Friedman