FOM: 74:Reverse arithmetic beginnings
Harvey Friedman
friedman at math.ohio-state.edu
Wed Dec 22 08:33:56 EST 1999
GENERAL REMARKS
After these general remarks, there is a detailed abstract.
In posting #73, we raised the question of whether Hilbert's program be
carried out in an extremely strong sense despite Godel's second
incompleteness theorem.
We said that in order to give convincing refutations of this, we need to
construct formal systems whose axioms are all standard assertions from the
literature, which cannot be proved consistent by various methods. This is
much more difficult to do than one would normally imagine.
Below, we present our first example of such a refutation - or at least it
lays the groundwork for more substantial refutations.
In particular, we give a strictly mathematical axiomatization of the formal
system of EFA = exponential function arithmetic - actually without even
using exponential notation!
All of the axioms except two are totally unassailable. The two that have to
be mulled over are axioms 16 and 17. (You may want to read HELP right after
the axioms are listed). I certainly have seen serious discussion of the
addition construction in 16, both in the discrete case and in the
continuous case.
However, 17 is not something I remember seeing that much, regardless of how
natural it is. Any comments on the appearance of the construction in 17 in
the actual literature would be greatly appreciated.
You may want to look at Remark iv) below. I don't like it as much because
of what I said in Remark iv) below, but I can use {1^2,2^2,3^2,...,n^2}
instead of axiom 17. This might ultimately be a good way to go.
Of course, all of this just scratches the surface. It may well turn out
that there is a much more spectacularly convincing way of doing this, and
there are many many candidates for truly spectacular results along these
lines that cannot be easily ruled out.
I am now looking at some comparably good ways to bootstrap this up to
higher logical strengths - at first staying within the context of finite
mathematics.
So what after all is Reverse Arithmetic? What is the base theory? Well, I'm
not quite sure yet, but there are several good looking possibilities in
light of this work. The problem is that under some formulations, it just
may be too difficult to get the results that one is looking for.
In particular, at the low end of base theories, obviously the axioms 1-13
of commutative ordered rings with unit plus the axiom of discreteness that
there is nothing strictly between 0 and 1 is very attractive - if something
really striking can be done. Here the language is simply 0,1,+,-,*,<,= of
ordered rings.
In posting #73, I mentioned these things:
1. Z is a discrete ordered ring.
2. The ax + by = 1 criteria for relative primeness.
3. The four squares theorem.
4. Every 1 <= i <= n divides n!
5. There is a prime between n and 2n.
6. FLT for exponents 3 and 4.
To keep the language in tact, one can replace 4 by
4'. For every n >= 1 there exists t such that every 1 <= i <= n is a
divisor of t.
The plan for this style of reverse arithmetic is twofold:
a) Show that statements such as 2,3,5,6 lead to a significant fragment of
bounded arithmetic over the base theory 1 (Z is a discrete ordered ring). I
can't say that one expects an equivalence with bounded arithmetic, since it
is expected that bounded arithmetic (i.e., ISigma_0) is not finitely
axiomatizable. So what is a significant fragment of bounded arithmetic?
Well, for the purposes of reverse arithemtic, that is not so clear.
b) However, ISigma_0(exp) = EFA is finitely axiomatizable. So perhaps
reverse arithmetic should start out with the goal of reversing statements
purely in the language of discrete ordered rings, with the discrete ordered
ring axioms as the base theory, up to the system EFA.
However this is something that I have not seen how to do in a striking way.
The results below employ variables over finite sets of integers. But before
moving to finite sets of integers in the setup, one should carefully
explore what can be done in the language of discrete ordered rings.
Instead of using the somewhat brutal 4', it would be very interesting to
use, say, the theory of Pell's equation.
So, it would be striking to have a set of facts like this:
1. Z is a discrete ordered ring (base theory).
2. Facts about linear congruences.
3. Facts about the structure of solutions to Diophantine equations such as
Pell's equation.
4. Diophantine equations with no solutions such as FLT for low exponents.
5. Facts about primes such as 5 above.
6. Irrationality of various algebraic numbers.
One gets the punch of exponentiation from 3. And if this proves too
difficult, then use the more blatant 4'.
If all this proves too difficult, then by all means add variables over
finite sets. Here we don't have the problem of the nonfinite
axiomatizability of ISigma_0 because we have beefed up the language.
So with variables over finite sets added to the language of discrete
ordered rings, it makes sense to take the following base theory B_0:
1. Z is a discrete ordered ring.
2. Axioms 14, 15, 18 below.
Then the goal is to try to find great literature facts which reverse to
ISigma_0 over B_0. I found axioms 16 and 17 for this purpose (see the
abstract below).
Also take the following stronger base theory B_1:
1. Z is a discrete ordered ring.
2. Axioms 14, 15, 18 below.
3. Axiom 19 below.
Then the goal is to try to find great literature facts which reverse to
ISigma_0(exp) over B_1. Again, axioms 16 and 17 do the trick (see the
abstract below).
In these two setups with variables over finite sets added to the language
of discrete ordered rings, the number of possibilities of spectacular
results is overwhelming. Practically any serious piece of number theory or
combinatorics is a candidate that needs to be looked at since in just about
any serious case, there are a myriad of explicit and implicit induction
arguments going on. Can they be reversed?? They are truly everywhere.
At the higher levels of reverse arithmetic, one can use my T_0 and T_1
below for base theories. Of course, one knows just what one is stepping off
of here metamathematically. They are equivalent to obvious versions of
ISigma_0 with variables over finite sets, and ISigma_0(exp) with variables
over finite sets.
**Mansucript available with proofs upon request.**
REVERSE ARITHMETIC BEGINNINGS
12/22/99
Let T_0 be the following system in the two sorted language with variables
over integers and variables over finite sets of integers. For the integer
sort, we use the language 0,1,+,-,*,= of rings. We use epsilon between
integers and sets. Equality is used only between integers.
1. Additive identity. x+0 = x.
2. Additive commutativity. x+y = y+x.
3. Additive associativity. x+(y+z) = (x+y)+z.
4. Additive inverse. x+(-x) = 0.
5. Multiplicative identity. x*1 = x.
6. Multiplicative commutativity. x*y = y*x.
7. Multiplicative associativity. x*(y*z) = (x*y)*z.
8. Distributivity. x*(y+z) = (x*y)+(x*z).
9. Linearity. x = 0 or 0 < x or 0 < -x.
10. Additive positivity. (0 < x and 0 < y) implies 0 < x+y.
11. Multiplicative positivity. (0 < x and 0 < y) implies 0 < x*y.
12. Unit positivity. 0 < 1.
13. Irreflexivity. not(0 < 0).
14. Finite intervals. (therexists A)(forall x)(x epsilon A iff (y < x and x
< z)).
15. Boolean difference. (therexists C)(forall x)(x epsilon C iff (x epsilon
A and not(x epsilon B)).
16. Set addition. (therexists C)(forall x)(x epsilon C iff (therexists
y)(therexists z)(y epsilon A and z epsilon B and x = y+z)).
17. Set multiplication. (therexists C)(forall x)(x epsilon C iff
(therexists y)(therexists z)(y epsilon A and z epsilon B and x = y*z)).
18. Least elements. (therexists x)(x epsilon A) implies (therexists x)(x
epsilon A and ((forall y)(y epsilon A implies not(y < x)).
T_1 consists of T_0 together with the following.
19. Common multiples. (therexists x)(0 < x and (forall y)((y epsilon A and
0 < y) implies (therexists z)(x = y*z))).
HELP: These very simple axioms may be hard to read in e-mail format, so we
remark that 1-13 are the usual axioms of commutative ordered ring with
unit, 14 says that the open intervals (x,y) exist, 16 says that the sum of
two sets exists, 17 says that the multiplication of two sets exists, 18
says that every nonempty set has a least element, 19 says that the positive
elements of every finite set have a positive common multiple.
REMARKS:
i) The intended interpretation of the set variables is finite sets of
integers. However, there is no axiom in T_0 that forces the sets to be
finite; e.g., the actual ring of integers together with all sets of
integers forms a model of T_0. However, axiom 19 in T_1 does rule that out.
In fact, obviously T_1 proves that every set is contained in some interval
[-x,x]. We could add that axiom explicitly to T_0 and our results would not
be affected.
ii) With the help of 18, it is easy to prove in T_0 that the interval (0,1)
is empty (the usual axiom of discreteness).
iii) Undoubtedly we can weaken some of 1-13 a bit since we have 18 (and the
rest). We have observed that we can weaken 19 to the special case where A =
{1,...,n} and get the same theory T_1. I.e., weaken it to "for all n > 0
there is a t > 0 which has every 0 < i <= n as a divisor."
iv) We can replace axiom 17 with the axiom asserting that for all n > 0,
{i^2: 1 <= i <= n} exists, and get an equivalent form of T_0 and T_1.
However, I prefer the present 17 since it is so much like 16 and their is a
pattern throughout the axioms of treating multiplication and addition
analogously for many purposes.
v) Below, ISigma_0 is the standard system of bounded induction; see
Hajek/Pudlak. And ISigma_0(exp) is EFA = exponential function arithmetic.
Also see Hajek/Pudlak.
THEOREM 1. T_0 is equivalent to ISigma_0 in the following sense. A formula
is provable in ISigma_0 if and only if its relativization to the x with
not(x < 0) is provable in T_0.
In fact, T_0 proves more induction than is indicated in Theorem 1.
THEOREM 2. T_0 proves induction for all formulas in the language of T_0
where all quantifiers are integer quantifiers that are bounded to integer
terms.
The point of Theorem 2 is that set parameters can be accomodated in bounded
induction.
THEOREM 3. T_1 is equivalent to ISigma_0(exp) = EFA in the following sense.
A sentence is provable in ISigma_0(exp) if and only if its relativization
to the x with not(x < 0) is provable in T_1.
In fact, T_1 proves more induction than is indicated in Theorem 3.
THEOREM 4. T_1 proves induction for all formulas in the language of T_1
where all quantifiers are bounded integer quantifiers (where an integer
term bound is placed on the integer variable being quantified) or bounded
set quantifiers (where an integer term bound is placed on the elements of
the set variable being quantified).
THEOREM 5. ISigma_0(exp) = EFA is interpretable in T_1 and vice versa.
**********
This is the 74th 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/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
More information about the FOM
mailing list