[FOM] 706: Second Incompleteness/1

Mon Sep 5 02:03:30 EDT 2016

Previously on FOM, we see

165: Incompleteness Reformulated  4/29/03  1:42PM
http://www.cs.nyu.edu/pipermail/fom/2003-April/006441.html

Godel's Theorems  4/29/03  9:57PM
http://www.cs.nyu.edu/pipermail/fom/2003-April/006443.html

166: Clean Godel Incompleteness  5/6/03  11:06AM
http://www.cs.nyu.edu/pipermail/fom/2003-May/006496.html

167: Incompleteness Reformulated/More  5/6/03  11:57AM
http://www.cs.nyu.edu/pipermail/fom/2003-May/006504.html

168: Incompleteness Reformulated/Again 5/8/03  12:30PM
http://www.cs.nyu.edu/pipermail/fom/2003-May/006518.html

174: Directly Honest Second Incompleteness  6/3/03  1:39PM
http://www.cs.nyu.edu/pipermail/fom/2003-June/006694.html

284: Godel’s Second  5/9/06  10:02AM
http://www.cs.nyu.edu/pipermail/fom/2006-May/010524.html

285: Godel’s Second/more  5/10/06  5:55PM
http://www.cs.nyu.edu/pipermail/fom/2006-May/010529.html

286: Godel’s Second/still more  5/11/06  2:05PM
http://www.cs.nyu.edu/pipermail/fom/2006-May/010532.html

305: Proofs of Godel’s Second  12/21/06  11:31AM
http://www.cs.nyu.edu/pipermail/fom/2006-December/011214.html

306: Godel’s Second/more  12/23/06  7:39PM
http://www.cs.nyu.edu/pipermail/fom/2006-December/011223.html

307: Formalized Consistency Problem Solved  1/14/07  6:24PM
http://www.cs.nyu.edu/pipermail/fom/2007-January/011282.html

343: Goedel’s Second Revisited 1  5/27/09  6:07AM
http://www.cs.nyu.edu/pipermail/fom/2009-May/013753.html

344: Goedel’s Second Revisited 2  6/1/09  9:21PM
http://www.cs.nyu.edu/pipermail/fom/2009-May/013778.html

346: Goedel’s Second Revisited 3  6/16/09  11:04PM
http://www.cs.nyu.edu/pipermail/fom/2009-June/013828.html

347: Goedel’s Second Revisited 4  6/20/09  1:25AM
http://www.cs.nyu.edu/pipermail/fom/2009-June/013837.html

348: Goedel’s Second Revisited 5  6/22/09  11:00AM
http://www.cs.nyu.edu/pipermail/fom/2009-June/013843.html

388: Goedel’s Second Again/definitive?  1/7/10  11:06AM
http://www.cs.nyu.edu/pipermail/fom/2010-January/014290.html

580: Goedel’s Second Revisited  5/29/15  5:52 AM
http://www.cs.nyu.edu/pipermail/fom/2015-May/018750.html

Explaining Some Goedel  4/18/16  11:06PM
http://www.cs.nyu.edu/pipermail/fom/2016-April/019745.html

There is also this detailed ms:

H. Friedman, Goedel's Second Theorem: Its Meaning and Use, March 17, 2012.
https://u.osu.edu/friedman.8/files/2014/01/GodelSecond0311712+08-19owppu.pdf

We rework these developments here in a clearer and more systematic
manner, with new results. The fundamental idea which is already
present in these documents as early as ?, is to use Goedel's
Completeness Theorem to recast (statements of) Goedel's Second
Incompleteness Theorem.

In this posting and the next two postings, we only consider rigorously
formulated versions of Second Incompleteness over PA and fragments.
I.e., in this and the next two postings, we should cover sections 1-3
in the outline below. In the interest of length, in this posting we
will only cover some of 1 and the part of 2 for PA. After these first
three postings, we should get into sections 4,5,6, and hopefully also
address proof theoretic issues yet later.

But I want to emphasize here that we are only concerned with rigorous
FORMULATIONS. I am not saying anything new here about proofs of GSIT.
We do give proofs of the new No Interpretation forms of GSIT, but
these proofs rely on standard GSIT. This of course creates issues,
since the usual formulations of standard GSIT are not rigorous.
Nevertheless, people (including me) have been confidently applying
usual forms of standard GSIT for various purposes with full
confidence, and we will follow that lead here. We anticipate dealing
with such proof theoretic issues in later postings.

As far as proofs of GSIT go, there is a weaker form of GSIT for which
the proofs are very satisfactory from many points of view. This is the
theorem that no consistent adequate system proves its 1-consistency.
The usual GSIT is proved by a mysterious diagonalization argument
together with a lot of care. This weak GSIT is proved by a transparent
diagonalization argument with much less care. Furthermore, in the
proof of this weak GSIT, one associates a clear mathematical object to
T and proves that the mathematical object corresponding to T +
1-Con(T) is different (bigger). I do not know of any such clear
mathematical assignment to T that is different for T + Con(T). I
suspect that this can be done in an interesting way, but I have not
seen it.

SECOND INCOMPLETENESS
September 5, 2016

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

The usual forms of GSIT = Goedel's Second Incompleteness Theorem take
the following general form:

GSIT. Let T be an adequate system in the first order predicate
calculus with equality. T does not prove its own consistency.

One often sees a correct and rigorously formulated notion of "adequate
system". However, one less often sees any explanation of what Con(T)
is as a sentence in the language of T. In order to even think of GSIT
as rigorously formulated, one is tacitly thinking of a formulation
like this:

GSIT. Let T be an adequate system in the first order predicate
calculus with equality. T does not prove Con(T), where Con(T) is any
naturally formalized sentence in the language of T expressing that T
is consistent.

The problem is that no two scholars on the planet would ever come up
with the same actual natural formalization, Con(T). There is of course
the compelling instinct that they would come up with formalizations
Con(T) which are demonstrably equivalent within very weak systems. In
this sense, we regard GSIT as (partly) informal. The aim here is to
replace (various forms of) GSIT with comparatively simple transparent
fully formal theorems which directly imply standard (forms of) GSIT.

The matter was addressed in a comparatively complicated way by Hilbert
Bernays with their so called Derivability Conditions. These provide a
sufficient condition for statements Con(T) in GSIT, for a wide range
of systems T. It has been simplified, and a comparatively manageable
account is presented in

H. Friedman, My Forty Years On His Shoulders. Horizons of Truth,
Proceedings of the Goedel Centenary, Cambridge University Press,
339-432, 2011.
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#58. Second on The Second Incompleteness Theorem.

A proposal to pin down consistency statements up to provable
equivalence is presented in

S. Feferman, Finitary inductively presented logics, in Logic
Colloquium '88, pp. 191-220, North Holland, Amsterdam, 1989; reprinted
in What is a Logical System? (D. S. Gabbay, ed.), Clarendon Press,
Oxford (1994), 297-328.
https://math.stanford.edu/~feferman/papers/presentedlogics.pdf

In both the Hilbert Bernays and Feferman approaches, subtle conditions
are required that go into the structure of consistency statements. So
we obtain awkwardly complex rigorous formulations of GSIT.

In our approach, we instead simply assert that certain kinds of
interpretations do not exist. The idea is that, whatever consistency
statements are, exactly, if they are provable (GSIT says that they are
not), then they will readily provide the nonexistent interpretations.

Also, in section 6, we go further and characterize consistency
statements up to provable equivalence by their memorable uses in
formulations of Goedel's Completeness Theorem.

Although Feferman's approach in the above is not a compelling way to
achieve what is claimed here, nevertheless Feferman is grappling with
a subtle issue that deserves further attention. Namely, toward a
general approach that explains what naturalness means in a wide
variety of inductive settings, arising from the given inductive
character. In such general circumstances, we are not going to have
some deep connections with iconic theorems like the Goedel
Completeness Theorem to lean on, as we do here.

We do need to make the bridge from our no interpretation theorems to
standard forms of GSIT. These bridge arguments are done through
formalized versions of Goedel's Completeness Theorem in section 2.

All theories discussed here are in the usual first order predicate
calculus with equality, with any set of symbols allowed. We use the
system PA of Peano Arithmetic with the primitives 0,S,+,x. We also use
the system EFA = exponential function arithmetic, with the primitives
0,S,+,x,exp,<. This  is also referred to as ISigma_0(exp). We also use
PFA = polynomial function arithmetic, with the primitives 0,S,+,x,<.
This is also referred to as bounded arithmetic, or ISigma_0  In
addition, we use SEFA = superexponential function arithmetic, which is
the natural extension of EFA to incorporate superexponentiation, with
the primitives 0,S,+,x,exp,superexp,<.

2. INTERPRETATION THEOREMS

This section relies entirely on the informal notion of  "natural
formalization of consistency statements" within PA and weaker systems.

All theories considered here are given by a fragment of the full
language of FOL (first order predicate calculus with equality), and a
set of sentences in that fragment. The fragment is required to have
equality, =, but may have none, finitely many, or even infinitely many
constants, relations, and function symbols. In models and
interpretations, equality must be treated as actual identity, and
interpretations are one dimensional. Reasonable variations from these
conventions will not make any difference for the results.

Formulas use variables v_n, n >= 0, connectives not, and, or, implies,
iff, and quantifiers forall, therexists.

We work in a relatively high level of generality, using r.e. presented
theories, which we now define. Here we view the nonlogical symbols of
FOL as appropriately indexed by nonnegative integers in the usual way.
Thus constant symbols are singly indexed, and relation and function
symbols are doubly indexed, one index indicating the rarity, and the
other indicating the copy number.

A theory consists of a language together with axioms. The language is
any set of constants, relations, and function symbols, via their
index, together with the required =. The axioms consist of any set of
sentences in the language. An r.e. presented theory is a Turing
machine which generates the language and the set of axioms which are
sentences within that language.

For r.e. presented T, we use the informal notion of "natural
formalization of Con(T) in PA". We will also use this notion for
systems substantially weaker than PA. Obviously, as the systems get
much weaker, the informal notion becomes more problematic, and
requires more explanation. At PA level and for a while down, we can
safely rely on standard intuition, and give essentially no further
explanation.

In this section, we focus on Goedel's Completeness Theorem, where we
show that Con(T), naturally formalized over PA and fragments, is
strong enough to interpret T in the context of PA and fragments. For
PA, the development is widely known, and the situation can be handled
comparatively crudely. Still some complications arise from using r.e.
presented T rather than finitely axiomatized T. As PA is replaced by
weaker and weaker systems, the development is less widely known, and
the situation has to be handled with more finesse.

Let T be a theory. A complete diagrammatic model of T is a consistent
set T* of sentences in the language L(T)* consisting of L(T) together
with a special nonempty set K of new constants, such that
i. T* includes T.
ii. T* is consistent in the version of predicate calculus with
equality based on L(T)*.
iii. Every sentence in L(T)* or its negation lies in T*.
iv. For every element (therexists v)(phi) of T*, there is a special
constant c in K such that phi[v/c] is in T*.
v. For distinct c,d in K, not(c = d) lies in T*.

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: We work in PA + Con(T). Let L be the language of T together
with infinitely many new constants d_,0,d_1,..., of ten called Henkin
constants. Hence although T lives in FOL, we will be working with
FOL(d_0,d_1,...) with its usual axioms and rules. We need to first
show that since T is consistent in FOL, T is also consistent in
FOL(d_0,d_1,...), which is straightforward.

We first generate the axioms of T as follows. Each phi_n is the axiom
of T generated by the r.e. presentation of T at stage n if it exists;
otherwise (forall v_0)(v_0 = v_0).  (Equality is taken for granted, so
each phi_n exists). We now generate the sentences of L as follows each
psi_n is the sentence with least goedel number that has not yet been
produced, which is in the language generated by the r.e. presentation
of T before stage n. In addition, we generate the axioms of T as
follows.

For the main construction, we produce an infinite sequence
rho_0,,rho_1,... of sentences in L as follows. rho_3n = phi_n.
rho_3n+1 = psi_n if {rho_0,...,rho_n-1,psi_n} is formally consistent;
not(psi_n) otherwise. We now define rho_3n+2. Let i < 3n+2 be least
such that rho_i begins with therexists and no sentence witnessing the
existential quantifier is among rho_0,...,rho_3n+1. Then rho_3n+2 is
the sentence that witnesses the existential quantifier with the least
Henkin constant that has not yet appeared. If i does not exist, set
rho_3n+2 = rho_3n+1.

We see that in PA, we can carry out this construction, by induction.
We have a low level arithmetic description of the construction.

Unfortunately, this construction only obeys conditions i-iv for a
complete diagrammatic model of T. We fix this problem as follows. For
each constant d_i, let gamma(d_i) be the d_j with least j such that
d_i = d_j is among the rho's. We now go through the rho's and replace
every d_i by gamma(d_j). Now we have a complete diagrammatic model of
T where K is the range of gamma. QED

We now discuss interpretations. We take the semantic approach to
interpretations, as it is the most conceptually clear. There is a
corresponding syntactic treatment that is well known to be equivalent.

Let T,W be theories. An interpretation pi of T in W consists of the following.
i. A formula phi of L(W) with one free variable v, intended to carve
out the nonempty domain from the point of view of W.
ii. Formulas psi[c] in L(W) with one free variable v, for constant
symbols c of L(T), intended to interpret c from the point of view of
W.
iii. Formulas psi[R] in L(W) with n distinct free variables
w_1,...,w_n, for n-ary relation symbols R of L(T), intended to
interpret R from the point of view of W.
iv. Formulas psi[F] in L(W) with n+1 distinct free variables
w_1,...,w_n+1, for n-ary function symbols F of L(T), intended to
interpret F from the point of view of W.
v. For any model of W, i-iv interpreted in that model actually defines
a model of T.

In the syntactic approach, v is replaced by two clauses:

vi. W proves that i-iv define a structure in L(T); i.e., W proves that
each of the formulas in i-iv, individually, are as intended.
vii. For each axiom of T, W proves that that axiom holds in the
defined structure.

In the case where L(T) is infinite, there is no requirement of any
kind of uniformity here. L(W) is not expected to recognize any
statements involving infinitely many symbols.

In this syntactic approach, we need to construct the sentence in L(W)
that expresses that a given sentence in L(T) holds in the defined
structure. This is of course somewhat tedious. The construction must
be made for formulas, and not just sentences. Given phi in L(T) there
is an associated formula pi(phi) in L(W) with the same free variables
such that for any structure S in L(W), pi(phi) holds in the S defined
L(T) structure at domain elements (which are among the domain elements
of S) if and only if phi holds in S at those same elements. Then vii
takes the form

vii'. For each axiom phi of T, W proves pi(phi).

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: We argue in W. Let W provably define a complete diagrammatic
model CDM of T. We build a structure in in what we think, sitting in
W, is L(T). For the domain, we use K. To interpret any constant c,
regardless of whether it is in K, use the unique c' in K such that c =
c' is in CDM. To interpret any n-ary relation symbol R, use
R*(c_1,...,c_n) iff R(c_1,...,c_n) is in CDM. To interpret any n-ary
function symbol F, use the definition of the n-ary function from
constants in K into constants in K given by F*(c_1,...,c_n) = c_n+1
iff F(c_1,...,c_n) = c_n+1 is in CDM. This defines a structure CDM* in
L(T) according to W.

We now have a possible satisfaction relation for CDM*, between
formulas and assignments to its free variables, all according to W.
Namely, if you plug in the assignment, thereby creating a sentence in
L(T), then that sentence lies in CDM. It is clear that, according to
W, this satisfaction relation for CDM* is correct - i.e., satisfies
the Tarski conditions.

We now define the interpretation pi of T in W. Let M be any model of
W. We take CDM* and restrict its language to L(T). Note that the
language of CDM* is the language L(T) according to M. So we are really
taking the standard part of this language. Note that because T is r.e.
presented, the language of L(T) according to M, includes the actual
L(T). Also, M thinks that CDM* satisfies every sentence that it thinks
is an axiom of T. These include the actual axioms of T, and M must
think that they are not only satisfied in CDM*, but also in CDM*
restricted to actual L(T). QED

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.

TO BE CONTINUED.

***********************************************
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 706th 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

Harvey Friedman