FOM: 61:Finitist proofs of conservation
Harvey Friedman
friedman at math.ohio-state.edu
Wed Sep 29 11:52:47 EDT 1999
This is the 61st in a series of self contained postings to fom covering a
wide range of topics in f.o.m. Previous ones are:
1:Foundational Completeness 11/3/97, 10:13AM, 10:26AM.
2:Axioms 11/6/97.
3:Simplicity 11/14/97 10:10AM.
4:Simplicity 11/14/97 4:25PM
5:Constructions 11/15/97 5:24PM
6:Undefinability/Nonstandard Models 11/16/97 12:04AM
7.Undefinability/Nonstandard Models 11/17/97 12:31AM
8.Schemes 11/17/97 12:30AM
9:Nonstandard Arithmetic 11/18/97 11:53AM
10:Pathology 12/8/97 12:37AM
11:F.O.M. & Math Logic 12/14/97 5:47AM
12:Finite trees/large cardinals 3/11/98 11:36AM
13:Min recursion/Provably recursive functions 3/20/98 4:45AM
14:New characterizations of the provable ordinals 4/8/98 2:09AM
14':Errata 4/8/98 9:48AM
15:Structural Independence results and provable ordinals 4/16/98
10:53PM
16:Logical Equations, etc. 4/17/98 1:25PM
16':Errata 4/28/98 10:28AM
17:Very Strong Borel statements 4/26/98 8:06PM
18:Binary Functions and Large Cardinals 4/30/98 12:03PM
19:Long Sequences 7/31/98 9:42AM
20:Proof Theoretic Degrees 8/2/98 9:37PM
21:Long Sequences/Update 10/13/98 3:18AM
22:Finite Trees/Impredicativity 10/20/98 10:13AM
23:Q-Systems and Proof Theoretic Ordinals 11/6/98 3:01AM
24:Predicatively Unfeasible Integers 11/10/98 10:44PM
25:Long Walks 11/16/98 7:05AM
26:Optimized functions/Large Cardinals 1/13/99 12:53PM
27:Finite Trees/Impredicativity:Sketches 1/13/99 12:54PM
28:Optimized Functions/Large Cardinals:more 1/27/99 4:37AM
28':Restatement 1/28/99 5:49AM
29:Large Cardinals/where are we? I 2/22/99 6:11AM
30:Large Cardinals/where are we? II 2/23/99 6:15AM
31:First Free Sets/Large Cardinals 2/27/99 1:43AM
32:Greedy Constructions/Large Cardinals 3/2/99 11:21PM
33:A Variant 3/4/99 1:52PM
34:Walks in N^k 3/7/99 1:43PM
35:Special AE Sentences 3/18/99 4:56AM
35':Restatement 3/21/99 2:20PM
36:Adjacent Ramsey Theory 3/23/99 1:00AM
37:Adjacent Ramsey Theory/more 5:45AM 3/25/99
38:Existential Properties of Numerical Functions 3/26/99 2:21PM
39:Large Cardinals/synthesis 4/7/99 11:43AM
40:Enormous Integers in Algebraic Geometry 5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees 5/25/99 5:11PM
43:More Enormous Integers/AlgGeom 5/25/99 6:00PM
44:Indiscernible Primes 5/27/99 12:53 PM
45:Result #1/Program A 7/14/99 11:07AM
46:Tamism 7/14/99 11:25AM
47:Subalgebras/Reverse Math 7/14/99 11:36AM
48:Continuous Embeddings/Reverse Mathematics 7/15/99 12:24PM
49:Ulm Theory/Reverse Mathematics 7/17/99 3:21PM
50:Enormous Integers/Number Theory 7/17/99 11:39PN
51:Enormous Integers/Plane Geometry 7/18/99 3:16PM
52:Cardinals and Cones 7/18/99 3:33PM
53:Free Sets/Reverse Math 7/19/99 2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry 8/27/99 3:01PM
57:Fixpoints/Summation/Large Cardinals 9/10/99 3:47AM
57':Restatement 9/11/99 7:06AM
58:Program A/Conjectures 9/12/99 1:03AM
59:Restricted summation:Pi-0-1 sentences 9/17/99 10:41AM
60:Program A/Results 9/18/99 1:32PM
John Burgess has specifically asked about whether one give a finitistic
model theoretic proof of certain conservative extension results discussed
in [Si99].
Burgess asks this in connection with Hilbert's program. Specifically,
I. WKL_0 is a conservative extension of PRA for Pi-0-2 sentences.
II. ACA_0 is a conservative extension of PA for arithmetic sentences.
III. ATR_0 is a conservative extension of IR for arithmetic sentences.
IV. Pi-1-1-CA_0 is a conservative extension of ID(<omega) for
arithmetic sentences.
Here IR is Feferman's IR, which can be taken to be the theory extending
PA with new function symbols encoding the Kleene H-sets on each
specific initial segment of the ordinal notation system Gamma_0.
All of these conservative extension results are given model theoretic
proofs in [Si99] except for III. The reader is referred to the
exposition of my proof in Friedman, MacAloon, Simpson, "A finite
combinatorial principle which is equivalent to the 1-consistency of
predicative analysis", 1982, 197-230 in: G. Metakides (ed.), Patras
Logic Symposion, Studies in Logic and the Foundations of mathematics,
North-Holland, 1982.
These model theoretic proofs are naturally and straightforwardly directly
formalized in ACA and in fact, in a little weaker system lying properly
between ACA_0 and ACA called ACA0+ in [Si99]. In particular, they are not
obviously formalized in ACA_0. So some work is needed to prove them in a
weak arithmetic system. Here we prove them in the weak system of arithmetic
called EFA* (see below), and show that EFA* is best possible.
More specifically, we write PFA (polynomial function arithmetic) for the
system in the language of 0,1,+,x,<, with the usual successor axioms and
defining
equations, together with induction for all bounded formulas. This is the
same as what is called ISigma_0 in the book {HP93] and elsewhere.
In [HP93], it is proved that PFA is fully capable of developing finite
sequence coding and formalizing syntax. In fact, they devote all of
Chapter V, section 3, to this topic, which is entitled "Exponentiation,
Coding Sequences and Formalization of Syntax in ISigma_0." In the
Bibliographic Notes on page 406, they write "A formalization of syntax
in ISigma_0 is considered here for the first time, though the ideas on
which it is based have been around for some time."
This makes PFA a good vehicle for taking a reverse mathematics point of
view towards weak fragments of arithmetic.
>From this point of view, it is natural to take EFA = exponential
function arithmetic to be in the language of PFA, whose axioms are PFA
plus the single axiom (forall n)(2^n exists). (From some points of view it
is more natural to take exponentiation as primitive). And we take EFA* to be
PFA plus the axiom that asserts that for all n, there is a sequence of
integers of length n, starting with 0, where each term is the base 2
exponentiation of the preceding term.
Here is what we will do in this note.
1. We isolate a crucial general fact about theories, which we call the
Key Lemma. The Key Lemma has an easy model theoretic proof. But the Key
Lemma also has a proof using the Criag interpolation theorem for
predicate calculus with equality. The interpolation theorem has model
theoretic proofs, but it also has a proof theoretic proof using
Gentzen's cut elimination theorem for predicate calculus with equality.
The usual proof of the cut elimination theorem with iterated
exponential estimates (given by Gentzen) is readily formalized in EFA*.
This yields a proof of the interpolation theorem and of the Key Lemma
that is readily formalized in EFA*.
2. Using the Key Lemma, we give a purely model theoretic proof the
conservation results in question. In fact, we adapt the usual model
theoretic proofs of these conservation results to provide formal
interpretations of the appropriate kind which establish the
conservation results. The Key Lemma is crucial.
3. We round out the situation by claiming that EFA* is best possible in
the following sense. That each of the conservation results are provably
equivalent to EFA* over PFA. By the way, the cut elimination theorem for
predicate calculus is also equivalent to EFA* over PFA.
**********
1. THE KEY LEMMA
THEOREM 1.1. Let T be a theory in predicate calculus whose language
includes <,=,c, and which contains the axioms of linear order. Suppose
that for each n >= 0, T is consistent with "there are at least n
elements << c." Let I be a new monadic predicate symbol. Then T + "I is
a cut below c" is consistent.
Proof: The model theoretic proof is straightforward. Consider T' = T
together with the axioms c > c_1 > c_2 > ..., where the c_i are new
constant symbols. Then T' is consistent. Let M be a model of T'. There
is obviously a cut below c in M. Set I to be a cut below c in M. Then
(M,I) satisfies T + "I is a cut below c." QED
Let W be the following theory in the language {<,=,0,S}:
a) axioms of linear order;
b) 0 is the least element;
c) Sx is the successor of x;
d) every nonzero element is the successor of some element.
There is a well known elimination of quantifiers for W. From this
elimination of quantifiers, one can also show that every formula phi(x)
in one free variable is provably equivalent over W to a Boolean
combination of inequalities of the form x < S...S0.
KEY LEMMA. Let T be a finitely axiomatized theory in predicate calculus
whose language includes <,=,0,c, and which contains the axioms of W.
Suppose that for each n >= 0, T is consistent with "there are at least
n elements < c." Let I be a new monadic predicate symbol. Then T + "I
is a cut below c" is consistent.
Proof: This is an immediate consequence of Theorem 1.1. But now we wish
to give an alternative proof using the Craig interpolation theorem for
predicate calculus with equality, and quantifier elimination for W.
Fix T,I to be as in the hypothesis of the Key Lemma, and assume that T
proves "I is not a cut below c." By the Craig interpolation theorem,
let phi be a sentence in the common language of T and "I is not a cut
below c" such that T proves phi and phi proves "I is not a cut below
c."
Hence phi is in the language {<,=,c} and has the following properties:
i) for all n >= 0, phi is consistent with W + "there are at least n
elements < c."
ii) phi proves "I is not a cut below c."
By cut elimination for W, there exists n >= 0 such that
phi if and only if c >= S^n(0)
is provable in W.
Let (K,<) be the linear ordering omega + Z, I = omega, and c lies in
Z. Then (K,<,I,c) satisfies W and therefore satisfies phi. But
(K,<,I,c) also satisfies "I is a cut below c." This contradicts that
phi implies "I is not a cut below c." QED
THEOREM 1.2. The Key Lemma is provable in EFA*.
Proof: We indicate the essential points. First of all, we have used the
interpolation theorem. One of the well known proofs goes as follows.
Let phi arrows psi be provable. Then phi arrows psi has a cut free
proof. And then an interpolant is constructed by recursion on the cut
free proof. There are no blowups in size after one obtains the cut free
proof.
The original proof by Gentzen of his cut elimination theorem coontained
iterated exponential estimates, and so is readily formalized in EFA*.
The cut elimination theorem for W is readily formalizable in EFA, which
is better than we need.
In the final steps, we considered the structure (K,<,I,c), where c
lies in Z. We used that satisfaction implies consistency, which in
general requires induction with respect to a truth predicate, and so
could be a problem in a system like EFA* with its limited induction.
However, because of the simplicity of the cut elimination procedure,
the truth predicate for this structure can be built up by simple
recursions. In fact, this can be carried out in EFA. Then the induction
needed for the final step is easily available in EFA. QED
More delicate arguments will also establish more general versions of
the Key Lemma in EFA*. In particular, with considerable effort, it can
be proved in EFA* with W replaced by the axioms for linear ordering
(and with 0 removed), as in Theroem 1.1. But the Key Lemma is precisely
what we need here.
2. WKL_0 OVER PRA
We use the following version of the usual Ackerman hierarchy of
functions from Z+ into Z+.
A_1(n) = 2n. A_i+1 is the indefinite iteration of A_i.
I.e., A_i+1(n) is the result of applying A_i n times starting at 1.
We need to consider a formalization of this hierarchy within PRA, or
even within EFA. We have to take into account the limited language of
PRA, and that no matter how this is formalized in PRA, we cannot prove
that the A's are total.
Let f(n) be the obvious algorithm for computing the n-th function in
the usual Ackerman hierarchy of functions using stacks. Specifically,
suppose the algorithm f(n) has been defined. The algorithm f(n+1)
computes at m by starting with 1, and applying the algorithm f(n) m
times.
Clearly f is a low level computable function. In PRA we cannot prove
that every f(n) is total; i.e., halts at all arguments. However, we can
obviously prove in PRA that
i) if f(n+1) is total and m < n then f(n) is total;
ii) if f(n+1) is total then f(n+1) is the indefinite iteration of f(n)
as in the usual Ackerman hierarchy of functions.
Here we have identified f(n) with the partial function that it
computes, which is a harmless abuse of terminology. Thus we will write
f(n)(m) for the output of the algorithm f(n) at the input m, which may
not be defined.
We now let phi be a Sigma-0-2 sentence that is consistent with PRA. We
want to show that phi is consistent with WKL0. Let phi = (therexists
p)(forall q)(R(p,q)). Fix p such that (forall q)(R(p,q)).
We let PRA' be PRA + phi + "f(c) is total." Since PRA proves f(n) is
total for each particular n, we see that the Key Lemma applies to PRA'.
Hence the system PRA'' = PRA + phi + "f(c) is total" + "I is a cut
below c" is consistent.
We now build a sequence of closed intervals [xi,yi], 0 <= i <= c/4.
For each such i, yi = f_c-2i(xi). We start with [x_0,y_0] = [p,f_c(p)].
Suppose [x_i,y_i] has been defined, yi = f_c-4i(x_i). Look at all Turing
machines with index <= fc-4i-2(x_i) which produce an output at 0 that
lies in [x_i,y_i]. Let E be the set of these at most f_c-4i-2(x_i) values.
By elementary combinatorial considerations, E must be disjoint from
some subinterval [x_i+1,y_i+1], where y_i+1 = f_c-2i-4(x_i+1), and x_i+1
> 2^(x_i). Take this to be [x_i+1,y_i+1]. The idea is that this choice of
the next interval is to handle all appropriate instances of Sigma-0-1
bounding whose front universal quantifier ranges over [0,x_i], and whose
parameters are subsets of [0,y_i+1].
Note that the left endpoints are strictly increasing and lie at or
above p. We now let J be the cut determined by looking at the left
endpoints whose index i lies in the cut I.
We now define an interpretation of WKL0 in PRA''. The integers are
taken to be the elements of J. And 0,<,+,x are are usual. From the
perspective of PRA'', take the sets to be the intersections of finite
sets with the cut J. Since J cannot be a finite set, we have the usual
overspill situation which allows us to prove the interpretation of weak
Konig's lemma and Delta-0-1 comprehension in PRA''. Also, the
interpretation of phi is obviously provable in PRA''. Every instance of
Sigma-0-1 induction becomes provable in PRA'' under this
interpretation; this has to be checked with set parameters. Hence WKL_0
+ phi is consistent since PRA'' is consistent.
THEROEM 2.1. EFA* proves that WKL_0 is conservative over PRA for Pi-0-2
sentences.
3. ACA_0 OVER PA
Let phi be an arithmetic sentence that is consistent with PA. Let R be
a binary relation symbol. Let T' be the following theory in the
language of PA together with c,R:
1) PA + phi;
2) for all i <= c, R(i,n) codes the i-th Turing jump.
3) induction for all formulas in the language.
Obviously, for all n, T' + c > n is consistent. We can therefore apply
the Key Lemma. Let T'' = T' + "I is a cut below c." Then T'' is
consistent.
We now define a translation of ACA_0 into T''. We take the arithmetic
part to be standard from the perspective of T''. We take the sets of
integers to be the sets of integers coded by the unary predicates
R(i,n) for i lying in I. We use 3) to verify that the interpretation of
the induction axiom of ACA_0 is provable in T''. And since T'' proves
that I is a cut below c, we see that the interpretation of each
instance of arithmetic comprehension is provable in T''.
THEOREM 3.1. EFA* proves that ACA_0 is conservative over PA for
arithmetic sentences.
4. ATR_0 OVER IR
IR amounts to the system ACA_0 + "for all x, the H-set starting with x on
each ordinal notation < Gamma_0 exists", where the statement in quotes is
taken as a scheme. We prove conservativity of ATR_0 over IR with respect to
Pi-1-1 sentences within EFA* as follows. Let alpha_0 < alpha_1 < ... be the
usual fundamental sequence approaching Gamma_0.
Let phi = (therexists x containedin omega)(psi(x)) be a Sigma-1-1 sentence
consistent with IR, where psi is arithmetical. Let P be a predicate symbol.
Let T be the following first order system (no set variables):
i) Peano arithmetic;
ii) for each i, we introduce a predicate symbol Q_i together with the
axioms asserting that Q_i is an H-set starting with P on alpha_i;
iii) transfinite induction on each alpha_i with respect to all formulas in
the language;
iv) psi(P).
Then T is consistent. Now let T' be in the language of arithmetic plus P
plus a new monadic predicate symbols Q,I plus the constant c. The axioms of
T' are T + "I is a cut below c" + "Q is an H-set starting with P on
alpha_c."
By the Key Lemma, T' is consistent. Then follow my model theoretic proof to
get the consistency of ATR_0 + psi(P), and hence of IR + phi.
5. Pi-1-1-CA_0 OVER ID(<omega)
We actually show in EFA* that every sentence of the form "p in O" that is
provable in Pi-1-1-CA_0 is provable in ID(<omega).
Let "p not in O" be consistent with ID(<omega). We can transfer over to
subsystems of second order arithmetic. Thus let T = ACA_0 + "the n-th
hyperjump exists" + "p not in O". Here the second axiom is a scheme over n,
and the third axiom is a specific sentence using a specific p. Then T is
consistent.
Let T' = ACA_0 + "the c-th hyperjump exists" + "p not in O." By the Key
Lemma, T'' = ACA_0 + "the c-th hyperjump exists" + "p not in O" + "I is a
cut below c" is consistent. Then define the obvious structure using the
sets coded up in the hyperjump hierarchies on the integers lying in the cut
I.
6. LENGTHS OF PROOFS
In each case we get a proof of the conservation result within EFA* that is
of normal length for a mathematical proof. This is because there is no
metamthametical argument used to prove the existence of a proof in EFA*.
Rather the proofs in EFA* are given explicitly. One does have to consider
relatizations of the four bigger theories (WKL_0, ACA_0, ATR_0,
Pi-1-1-CA_0) that come out of the translations that are defined in each
case. However, these theories are finitely axiomatized by formulas of
reasonable size.
One can consider lengths of proofs inherent in the conservation statements
themselves. The only nonlinear blowups involved occur in the conversion of
proofs with cut to proofs without cut in the predicate calculus. This is
well known to be a linear stack of 2's.
It is also well known that there is a linear stack of 2's blowup in this
cut elimination procedure. One of the proofs of this blowup can be
converted into a proof that this same blowup occurs in each of these four
conservation results.
These observations can also be converted to a proof within PFA that each of
these four conservation results are provably equivalent to EFA*.
REFERENCES
[Si99] Steve Simpson, Subsystems of Second Order Arithmetic, Persepctives
in Mathematical Logic, Springer, 1999.
[HP93] Petr Hajek and Pavel Pudlak, Metamathematics of First-Order
Arithmetic, Perspectives in Mathematical Logic, Springer, 1993.
More information about the FOM
mailing list