[FOM] 388: Goedel's Second Again/definitive?
Harvey Friedman
friedman at math.ohio-state.edu
Thu Jan 7 11:06:06 EST 2010
I have written about Goedel's Second in these FOM postings:
http://www.cs.nyu.edu/pipermail/fom/2003-May/006496.html
http://www.cs.nyu.edu/pipermail/fom/2003-May/006504.html
http://www.cs.nyu.edu/pipermail/fom/2003-May/006518.html
http://www.cs.nyu.edu/pipermail/fom/2003-June/006694.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010524.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010525.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010529.html
http://www.cs.nyu.edu/pipermail/fom/2006-May/010532.html
http://www.cs.nyu.edu/pipermail/fom/2006-December/011194.html
http://www.cs.nyu.edu/pipermail/fom/2006-December/011223.html
http://www.cs.nyu.edu/pipermail/fom/2007-January/011282.html
http://www.cs.nyu.edu/pipermail/fom/2009-May/013753.html
http://www.cs.nyu.edu/pipermail/fom/2009-May/013778.html
http://www.cs.nyu.edu/pipermail/fom/2009-June/013828.html
http://www.cs.nyu.edu/pipermail/fom/2009-June/013837.html
http://www.cs.nyu.edu/pipermail/fom/2009-June/013843.html
NOW it appears that I have identified a much clearer and much simpler
key sufficiency property on the formalizations of Con that ensure the
unprovability of Con.
1. SUFFICIENCY PROPERTY FOR FORMALIZATIONS OF CONSISTENCY.
Here is the key idea:
###For Goedel's Second Incompleteness Theorem, it is sufficient that
the formalization of consistency support the Goedel Completeness
Theorem###
We will use L = single sorted first order predicate calculus with
equality. Infinitely many constant, relation, and function symbols are
available.
Let K be a set of sentences in L. We define the notion
*a sufficient formalization of Con(K) in S*
where S is a set of sentences in L. This is a sentence psi in L(S)
such that there is a definition in L(S) of a structure (D,...) in
L(K), such that for every element rho of K, S proves
**psi implies '(D,E,...) satisfies rho'**
Here '(D,...) satisfies rho' is the sentence of L(S) defined
straightforwardly. Note that this definition is quite easy to make
fully rigorous - e.g., by induction on rho. The Intensionality Issues
that plague the usual statements of Goedel's Second Incompleteness
Theorem are NOT PRESENT HERE.
NOTE: Obviously if psi is a sufficient formalization of Con(K) in S,
and S proves psi implies gamma, then gamma is also a sufficient
formalization of Con(K) in S.
We now want to consider "the usual formalizations of Con(K) in
arithmetic". For this purpose, the natural system to use for S is EFA
= exponential function arithmetic = ISigma0(exp), which is based on
0,S,+,dot,exp,<=, with the usual axioms for successor, defining
equations for +,dot,exp, definition of <=, and induction for all
bounded formulas. EFA is the weakest natural system of arithmetic
which supports worry free arithmetization of syntax. In bounded
formulas in L(EFA), the quantifiers are bounded as follows.
(forall n <= t)
(therexists n <= t)
where t is a term of L(EFA) in which n does not appear. Note that
**the usual formalizations of Con(K) in L(EFA)**
makes good sense. We caution the reader that some important issues
will arise when K is infinite. It is well known that EFA is finitely
axiomatizable.
SEMIFORMAL THEOREM. Let K be a finite set of sentences in L. The usual
formalizations of Con(K) in L(EFA) are Pi01 sufficient formalizations
of Con(K) in EFA.
Here a Pi01 sentence in L(EFA) is a sentence in L(EFA) that begins
with one or more universal quantifiers, and is followed by a bounded
formula.
There are usual formalizations of Con(K) when K is infinite, PROVIDED
that K is recursively enumerable. These usual formalizations can be
based on any algorithm for generating the elements of K.
SEMIFORMAL THEOREM. Let K be a recursively enumerable set of sentences
in L. The usual formalizations of Con(K) in L(EFA) are Pi01 sufficient
formalizations of Con(K) in EFA.
Here a Pi01 sentence in L(EFA) is a sentence in L(EFA) that begins
with 0 or more universal quantifiers, which are followed by a founded
formula.
For which K are there (Pi01) sufficient formalizations of Con(K) in
EFA? In Q? All K, because 1 = 0 is a (Pi01) sufficient formalization
of Con(K) in EFA. The following is more informative.
THEOREM. Let K be a set of sentences in L. The following are equivalent.
i. There is a Pi01 sufficient formalization of Con(K) in Q which is
consistent with Q.
ii. There is a Pi01 sufficient formalization of Con(K) in EFA that is
consistent with EFA.
iii. There is a Pi01 sufficient formalization of Con(K) in Q that is
true.
iv. There is a Pi01 sufficient formalization of Con(K) in EFA that is
true.
v. K is a subset of a consistent recursively enumerable set of
sentences in L.
We caution the reader that this notion of sufficient formalization can
be very weak:
THEOREM. Let K be a set of sentences in L. Then any sentence provable
in K is a sufficient formalization of Con(K) in K.
2. GOEDEL'S SECOND INCOMPLETENESS THEOREM FOR ARITHMETIZED CONSISTENCY.
We remind the reader that the usual formalizations of Con(T) in
arithmetic involve arithmetizing finite sequences of nonnegative
integers. Accordingly, we now define EFA* to be EFA + "for all n,
there is a sequence of integers of length n starting with 2, where
each noninitial term is the base 2 exponential of the previous term".
GOEDEL'S SECOND INCOMPLETENESS THEOREM FOR CONSISTENCY FORMALIZED IN
EFA. Let T be a consistent set of sentences in L that implies EFA*. T
does not prove any Pi01 sufficient formalization of Con(T) in EFA.
We state another form, which is of mainly technical interest.
GOEDEL'S SECOND INCOMPLETENESS THEOREM FOR CONSISTENCY FORMALIZED IN
Q. Let T be a consistent set of sentences in L that implies EFA. T
does not prove any Pi01 sufficient formalization of Con(T) in Q.
Here Q is Raphael Robinson's Q. But for any T, the usual
formalizations of Con(T) in arithmetic definitely use exponentiation,
so we take the position that aren't any usual formalizations of Con(T)
in Q, or even PFA = polynomial function arithmetic = bounded
arithmetic = ISigma0. (It should be noted that there are usual
formalizations of Con(T) designed CAREFULLY BY SPECIALISTS in order to
"work in Q", and all of those are sufficient formalizations of Con(T)
in Q).
3. GOEDEL'S SECOND INCOMPLETENESS THEOREM FOR SEQUENCE THEORETIC
CONSISTENCY.
Goedel used arithmetized consistency statements. It is more natural
and direct to use sequence theoretic consistency statements. This has
many advantages.
We will use a very natural and very convenient system for the
formalization of syntax of L. We will call it SEQSYN (for sequence
syntax).
SEQSYN is a two sorted system with equality for each sort. It is
convenient (although not necessary) to use undefined terms. There is a
very good and standard way of dealing with logic with undefined terms.
This is discussed, with references to the literature, in
H. Friedman, The Inevitably of Logical Strength: strict reverse
mathematics, in: Logic Colloquium '06, ASL, p. , 2009.
In summary, two terms are equal (written =) if and only if they are
both defined and have the same value. two terms are partially equal
(written ~=) if and only if either they are equal or both are
undefined. If a term is defined then all of its subterms are defined.
The two sorts in SEQSYN are Z (for integers, including positive and
negative integers and 0), and FSEQ (for finite sequences of integers,
including the empty sequence). We have variables over Z and variables
over FSEQ (we use Greek letters). We use ring operations 0,1,+,-,dot,
the order <=, and = between integers. We use lth (for length of a
finite sequence, which returns a nonnegative integer), val(alpha,n)
(for the n-th term of the finite sequence alpha, which may be
undefined), and = between finite sequences. The nonlogical axioms of
SEQSYN are
i. The discrete ordered commutative ring axioms.
ii. Every alpha has a largest term.
iii. lth(alpha) >= 0.
iv. val(alpha,n) is defined if and only if 1 <= n <= lth(alpha).
v. alpha = beta if and only if for all n, (val(alpha,n) ~= val(beta,n)).
vi. Induction on the nonnegative integers for all bounded formulas.
vii. Let n >= 0 be given and assume that for all 1 <= i <= n, there is
a unique m such that phi(i,m). There exists a sequence alpha of length
n such that for all 1 <= i <= n, val(alpha,i) = m iff phi(i,m). Here
phi is a bounded formula in L(SEQSYN) in which alpha does not appear.
It remains to define the bounded formulas. We require that the integer
quantifiers be bounded in this way:
(forall n of magnitude at most t)
(therexists n of magnitude at most t)
where t is an integer term in which n does not appear.
We now come to a crucial point. We require that the sequence
quantifiers be bounded in this way:
(forall alpha whose length and terms are of magnitude at most t)
(therexists alpha whose length and terms are of magnitude at most t)
where t is an integer term in which alpha does not appear.
THEOREM. SEQSYN is mutually interpretable with Q and with PFA. SEQSYN
is interpretable in EFA but not vice versa.
So in the above sense, we claim that the usual string theoretic
formalizations of consistency carry a weaker commitment than the usual
arithmetic formalizations of consistency.
Note that SEQSYN does not have exponentiation, yet SEQSYN clearly
supports the usual string theoretic formalization of consistency.
SEMIFORMAL THEOREM. Let K be a recursively enumerable set of sentences
in L. The usual formalizations of Con(K) in L(SEQSYN) are Pi01
sufficient formalizations of Con(K) in SEQSYN.
Here a Pi01 sentence in L(SEQSYN) is a sentence in L(SEQSYN) that
begins with zero or more universal quantifiers of either sort, which
is followed by a bounded formula in the above sense.
THEOREM. Let K be a set of sentences in L. The following are equivalent.
i. There is a consistent sufficient formalization of Con(K) in SEQSYN
that is consistent with SEQSYN.
ii. There is a consistent sufficient formalization of Con(K) in SEQSYN
that is true.
iii. K is a subset of a consistent recursively enumerable set of
sentences in L.
We take EXP to be the following sentence in L(SEQSYN).
There exists a sequence alpha of length n >= 1 whose first term is 2,
where every noninitial term is twice the previous term.
THEOREM. SEQSYN + EXP and EFA are mutually interpretable. They are
both finitely axiomatizable.
GOEDEL'S SECOND INCOMPLETENESS THEOREM FOR CONSISTENCY FORMALIZED IN
SEQSYN. Let T be a consistent set of sentences in L that implies
SEQSYN + EXP. T does not prove any Pi01 sufficient formalization of
Con(T) in SEQSYN.
5. GOEDEL'S SECOND INCOMPLETENESS THEOREM FOR DIRECT SET THEORETIC
CONSISTENCY.
Let K be a finite set of sentences in epsilon,=. By the direct set
theoretic formalization of Con(K), we mean the following sentence in
set theory (epsilon,=):
there exists D,R, where R is a set of ordered pairs from D, such that
(D,E,R) satisfies each element of K.
Let RST (rudimentary set theory) be the following convenient set
theory in epsilon,=:
a. Extensionality.
b. Pairing.
c. Union.
d. Cartesian product.
e. Separation for bounded formulas.
It can be shown that RST is finitely axiomatizable.
GOEDEL'S SECOND INCOMPLETENESS THEOREM FOR DIRECT SET THEORETIC
CONSISTENCY. Let K be a consistent finite set of sentences in
epsilon,=, which implies RST. K does not prove the direct set
theoretic formalization of Con(K).
COROLLARY. Let K be a consistent set of sentences in epsilon,=, which
implies RST. There is some consequence phi of K such that K does not
prove the direct set theoretic formalization of Con(phi).
It does not appear that we can obtain Goedel's Second Incompleteness
Theorem for PA and fragments, in any reasonable form, from Goedel's
Second Incompleteness Theorem for Direct Set Theoretic Consistency.
**********************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 388th 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-349 can be found at http://www.cs.nyu.edu/pipermail/fom/2009-August/014004.html
in the FOM archives.
350: one dimensional set series 7/23/09 12:11AM
351: Mapping Theorems/Mahlo/Subtle 8/6/09 10:59PM
352: Mapping Theorems/simpler 8/7/09 10:06PM
353: Function Generation 1 8/9/09 12:09PM
354: Mahlo Cardinals in HIGH SCHOOL 1 8/9/09 6:37PM
355: Mahlo Cardinals in HIGH SCHOOL 2 8/10/09 6:18PM
356: Simplified HIGH SCHOOL and Mapping Theorem 8/14/09 9:31AM
357: HIGH SCHOOL Games/Update 8/20/09 10:42AM
358: clearer statements of HIGH SCHOOL Games 8/23/09 2:42AM
359: finite two person HIGH SCHOOL games 8/24/09 1:28PM
360: Finite Linear/Limited Memory Games 8/31/09 5:43PM
361: Finite Promise Games 9/2/09 7:04AM
362: Simplest Order Invariant Game 9/7/09 11:08AM
363: Greedy Function Games/Largest Cardinals 1
364: Anticipation Function Games/Largest Cardinals/Simplified 9/7/09
11:18AM
365: Free Reductions and Large Cardinals 1 9/24/09 1:06PM
366: Free Reductions and Large Cardinals/polished 9/28/09 2:19PM
367: Upper Shift Fixed Points and Large Cardinals 10/4/09 2:44PM
368: Upper Shift Fixed Point and Large Cardinals/correction 10/6/09
8:15PM
369. Fixed Points and Large Cardinals/restatement 10/29/09 2:23PM
370: Upper Shift Fixed Points, Sequences, Games, and Large Cardinals
11/19/09 12:14PM
371: Vector Reduction and Large Cardinals 11/21/09 1:34AM
372: Maximal Lower Chains, Vector Reduction, and Large Cardinals
11/26/09 5:05AM
373: Upper Shifts, Greedy Chains, Vector Reduction, and Large
Cardinals 12/7/09 9:17AM
374: Upper Shift Greedy Chain Games 12/12/09 5:56AM
375: Upper Shift Clique Games and Large Cardinals 1
376: The Upper Shift Greedy Clique Theorem, and Large Cardinals
12/24/09 2:23PM
377: The Polynomial Shift Theorem 12/25/09 2:39PM
378: Upper Shift Clique Sequences and Large Cardinals 12/25/09 2:41PM
379: Greedy Sets and Huge Cardinals 1
380: More Polynomial Shift Theorems 12/28/09 7:06AM
381: Trigonometric Shift Theorem 12/29/09 11:25AM
382: Upper Shift Greedy Cliques and Large Cardinals 12/30/09 2:51AM
383: Upper Shift Greedy Clique Sequences and Large Cardinals 1
12/30/09 3:25PM
384: THe Polynomial Shift Translation Theorem/CORRECTION 12/31/09
7:51PM
385: Shifts and Extreme Greedy Clique Sequences 1/1/10 7:35PM
386: Terrifically and Extremely Long Finite Sequences 1/1/10 7:35PM
387: Better Polynomial Shift Translation/typos 1/6/10 10:41PM
Harvey Friedman
More information about the FOM
mailing list