[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: 74:Reverse arithmetic beginnings*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Wed, 22 Dec 1999 08:33:56 -0500*Sender*: owner-fom@math.psu.edu

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

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]