FOM: 103:Hilbert's Program for Consistency Proofs/1

Harvey Friedman friedman at
Wed Apr 11 11:10:15 EDT 2001

NOTE: This concerns material that is part of a talk "The Future of Reverse
Mathematics" that I gave most recently at Simpson's special session on
Reverse Mathematics at the ASL annual meeting in Philadelphia.

Originally I had presented this material in the context of the refutation
of a doctrine I call "tamism". But I now believe that it is clearer and
more appropriate to place it in the context of a refutation of Hilbert's
program on consistency proofs.



Hilbert's program for consistency proofs was to provide a proof of the
consistency of comprehensive systems for mathematical reasoning such as
"analysis" as formalized by the two sorted first order system of second
order arithmetic, Z2, using comparatively "unimpeachable" reasoning, such
as "finitary reasoning."

It is generally considered that Godel's second incompleteness theorem put
an end to this program, at least without radically altering the vision of
the program.

However, it appears that there is a natural weakening of the Hilbert
program for consistency proofs - which we simply call Hilbert's program
here - that has not been focused on and can be used as the basis for a new
interesting line of research in f.o.m.

The new statement of Hilbert's program is

*to find a satisfactory model of mathematical practice which includes all
of the important or essential mathematics that has been proved, and
arguably will be proved, and show that under this model, no inconsistency
can arise,  using only unimpeachable methods*

We aim to definitively refute this new statement of Hilbert's program. The
refutations consist of showing that no such model and consistency proof can
be given. In particular, refutations take the form of showing that any
model of mathematical practice with certain properties cannot have a
consistency proof with certain properties.

Why doesn't the usual results about consistency proofs of a system such as
Peano Arithmetic already refute this  statement of Hilbert's program?

The answer is that the induction scheme can be criticized as being far too
general. After all, actual inductions used in important or essential
mathematics - or even just natural mathematics - are not general, and in
fact are rather special.

But what about, say, Sigma-0-1 induction? Although this is finitely
axiomatizable, it still can be criticized as being too general, and not at
all like the inductions that are actually used.

The fact of the matter is that no one has a good proposal for what the
"good" or "natural" inductions are. A similar remark applies to other kinds
of mathematical principles. Such a proposal is needed to actually carry out
this form of Hilbert's program.

But we aim to definitively refute this form of Hilbert's program. So the
fact that no one has a good proposal for carrying out this form of
Hilbert's program is besides the point.

What kind of results do we wish to obtain to make such refutations?

We seek to find finite sets of sentences representing "important" or
"essential" mathematics, which, without any additional axioms, form formal
systems which cannot be proved consistent by certain methods.

But how can we view a finite set of strictly mathematical sentences as a
formal system? We regard the finite sets as proper axioms over many sorted
predicate calculus.

This setup differs from the usual reverse mathematics setup as described in
Simpson's book, because there we use the base theory RCA0. RCA0 is not
entirely made up of "important" or "essential" mathematical statements.

We can view the present setup as "pure" reverse mathematics in that we have
no base theory per se - only pure logic is taken for granted.

But can't we go further and object to the use of many sorted first order
logic? After all, one can also say that mathematics does not use anything
like arbitrary first order formulas. We comment as follows.

a. Every appropriate model of mathematics must be dynamic, in the sense of
allowing for the continued development  of mathematics. Otherwise, we can
just go through the present mathematical literature and point out that no
contradiction has arisen, and therefore mathematics at present is
consistent. The consistency proof is obtained simply by looking at the
present literature.

b. There is a version of the predicate calculus which we call local
predicate calculus, where the formulas allowed are extremely limited. The
complexity of local predicate calculus is entirely based on the web of
abbreviations that are used. It is difficult to imagine what kind of
reasonable model of mathematical practice would not subsume the local
predicate calculus.

We will take up a presentation and discussion of the local predicate
calculus in a later installment.


In this section, we deal only with the issue of getting started, or
crossing the barrier between theories of an algebraic nature versus
theories of a classical metamathematical nature.

By getting started, we mean the presentation of a finite set of
mathematical statements arguably meeting our criterion of representing
"important" or "essential" mathematics, where the system I call exponential
function arithmetic, or EFA, is interpretable. EFA is the same as what is
normally called IDelta0(exp) - see Hajek and Pudlak book.

EFA is a singularly important finitely axiomatized fragment of PA where
coding and various metamathematical manipulations can readily be done. It
has variables over nonnegative integers only, with 0,1,+,x,<, as well as
two variable exponentiation. It has the usual defining equations, axioms
for successor, and definition of <. It also has induction with respect to
bounded formulas.

We have previously conjectured on the FOM that EFA suffices to prove all of
the celebrated results of number theory that are readily formalizable in
the language of arithmetic (or in finite set theory). In particular, we
conjecture that EFA proves Fermat's Last Theorem.

Getting started in the sense we mean here is not in itself sufficient to
give the sort of convincing refutation of Hilbert's program that we seek.
Hilbert would appropriately allow significantly more than EFA in his
arsenal of unimpeachable methods.

But the point is that, once we have secured EFA (even by interpretation),
we can presumably leapfrog to higher levels in an appropriately convincing

We give two alternative presentations, T1 and T2. In both cases, the
language consists of

a) variables over integers (positive and negative);
b) 0,1,+,-,dot,<,= in the integers. Dot is integer multiplication;
c) variables over FINITE sets of integers;
d) epilson among integers and finite sets of integers.

T1 consists of the following axioms:

1. Usual ordered ring axioms.
2. Boolean axiom. A\B = {x: x in A and x notin B}.
3. Open Intervals. (a,b) = {x: a < x < b} exists.
4. Every nonempty set has a least element.
5. Sum set. A+B = {x+y: x in A and y in B} exists.
6. Product set. A dot B = {x dot y: x in A and y in B} exists.
7. For all n > 0 there exists t > 0 such that for all 1 <= i <= n, i
divides t.

T2 consists of the following axioms:

1. Usual ordered ring axioms.
2. Boolean axiom. A\B = {x: x in A and x notin B}.
3. Finite Open Intervals. (a,b) = {x: a < x < b} exists.
4. Every nonempty set has a least element.
5. Sum sets. A+B = {x+y: x in A and y in B} exists.
6. Scalar set multiplication. c dot A = {c dot x: x in A} exists.
7. Squares. For all n, {i^2: 1 <= i <= n} exists.
8. For all n > 0 there exists t > 0 such that for all 1 <= i <= n, i
divides t.

The systems T1-,T2- are obtained by dropping the last axioms 7,8. They imply

i) (0,1) is empty;
ii) every set is included in some (a,b);
iii) the union and intersection of any two sets exist.

THEOREM 1. T1- = T2-, and T1 = T2. The first order sentences provable in
T1- are exactly the sentences that are provable in PFA (polynomial function
arithmetic) = IDelta0, when converted from the ordered ring Z to the
ordered semiring N in the standard way. The first order sentences provable
in T1 are exactly the sentences without exponentiation that are provable in
EFA, when converted from Z to N in the obvious way.

Note in particular that the first order part (consequences) of T1 is
finitely axiomatizable, since EFA is finitely axiomatizable.

THEOREM 2. EFA is uniquely interpretable in T1 via an interpretation that
is standard from the ordered ring Z to the ordered semiring N. T1 is a
definitional extension of the first order part of T1.


We give two alternative presentations, T3 and T4. In both cases, the
language consists of

a) variables over integers (positive and negative);
b) 0,1,+,-,dot,<,= in the integers. Dot is integer multiplication;
c) variables over FINITE sets of integers;
d) epilson among integers and finite sets of integers;
e) 2^x defined only for x >= 0. This is treated as a partial function symbol.

T3 consists of the following axioms:

1. Usual ordered ring axioms.
2. 2^0 = 1, 2^1 = 1+1, 2^(x+y) = 2^x dot 2^y.
3. 2^n is defined if and only if n >= 0.
4. Boolean axiom. A\B = {x: x in A and x notin B}.
5. Finite Open Intervals. (a,b) = {x: a < x < b} exists.
6. Every nonempty set has a least element.
7. Sum sets. A+B = {x+y: x in A and y in B} exists.
8. Scalar set multiplication. c dot A = {c dot x: x in A} exists.
9. Powers. For all n >= 0, {2^i: 0 <= i <= n} exists.

THEOREM 3. The first order part of T3 is exactly the same as EFA =
IDelta0(exp) formulated over Z with partial base 2 exponentiation. T3 is a
definitional extension of the first order part of T3.


We can extend T3 by introducing any new function symbols. It is most
convenient to have them be everywhere defined, using default values if
necessary. We assume that they are given quantifier free axioms only
(universally quantified). Then the key axioms that we add are that for each
n >= 0, the graph of each new function exists with arguments of absolute
value at most n. For functions F(x1,...,xk) that are multivariate, it is
most convenient to do this as follows:

*for all n >= 0 and a1,...,ak, {a1 dot x1 + ... + ak dot xk + b dot
F(x1,...,xk): -n <= x1,...,xk <= n} exists*

We would then get a system that corresponds to IDelta0(exp,F1,...,Fp).

E.g., we can do this for the usual defining equations for
superexponentiation, which is unary, or even for the defining equations for
the Ackermann function, which is binary. In the latter case, we obtain a
system that is not provably consistent within PRA or even RCA0.


 This is the 103rd 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
 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/17/99  1:32PM
 61:Finitist proofs of conservation  9/29/99  11:52AM
 62:Approximate fixed points revisited  10/11/99  1:35AM
 63:Disjoint Covers/Large Cardinals  10/11/99  1:36AM
 64:Finite Posets/Large Cardinals  10/11/99  1:37AM
 65:Simplicity of Axioms/Conjectures  10/19/99  9:54AM
 66:PA/an approach  10/21/99  8:02PM
 67:Nested Min Recursion/Large Cardinals  10/25/99  8:00AM
 68:Bad to Worse/Conjectures  10/28/99  10:00PM
 69:Baby Real Analysis  11/1/99  6:59AM
 70:Efficient Formulas and Schemes  11/1/99  1:46PM
 71:Ackerman/Algebraic Geometry/1  12/10/99  1:52PM
 72:New finite forms/large cardinals  12/12/99  6:11AM
 73:Hilbert's program wide open?  12/20/99  8:28PM
 74:Reverse arithmetic beginnings  12/22/99  8:33AM
 75:Finite Reverse Mathematics  12/28/99  1:21PM
 76: Finite set theories  12/28/99  1:28PM
 77:Missing axiom/atonement  1/4/00  3:51PM
 78:Qadratic Axioms/Literature Conjectures  1/7/00  11:51AM
 79:Axioms for geometry  1/10/00  12:08PM
 80.Boolean Relation Theory  3/10/00  9:41AM
 81:Finite Distribution  3/13/00  1:44AM
 82:Simplified Boolean Relation Theory  3/15/00  9:23AM
 83:Tame Boolean Relation Theory  3/20/00  2:19AM
 84:BRT/First Major Classification  3/27/00  4:04AM
 85:General Framework/BRT   3/29/00  12:58AM
 86:Invariant Subspace Problem/fA not= U  3/29/00  9:37AM
 87:Programs in Naturalism  5/15/00  2:57AM
 88:Boolean Relation Theory  6/8/00  10:40AM
 89:Model Theoretic Interpretations of Set Theory  6/14/00 10:28AM
 90:Two Universes  6/23/00  1:34PM
 91:Counting Theorems  6/24/00  8:22PM
 92:Thin Set Theorem  6/25/00  5:42AM
 93:Orderings on Formulas  9/18/00  3:46AM
 94:Relative Completeness  9/19/00  4:20AM
 95:Boolean Relation Theory III  12/19/00  7:29PM
 96:Comments on BRT  12/20/00  9:20AM
 97.Classification of Set Theories  12/22/00  7:55AM
 98:Model Theoretic Interpretation of Large Cardinals  3/5/01  3:08PM
 99:Boolean Relation Theory IV  3/8/01  6:08PM
100:Boolean Relation Theory IV corrected  11:29AM  3/21/01
101:Turing Degrees/1  3:32AM  4/2/01
102:Turing Degrees/2  5:20PM  4/8/01

More information about the FOM mailing list