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

*To*: fom@math.psu.edu*Subject*: FOM: 73:Hilbert's program wide open?*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Mon, 20 Dec 1999 20:28:26 -0500*Sender*: owner-fom@math.psu.edu

This discusses a new view of Hilbert's program together with an associated research program. 1. CONVENTIONAL APPROACHES. It is considered conventional wisdom, basic f.o.m., that Godel's second incompleteness theorem killed Hilbert's program. Historically, there have been complaints about this conclusion on the following grounds. That Hilbert may have accepted some sort of "extended" finitist reasoning such as Gentzen's use of quantifier free epsilon_0 induction, which he used to prove the consistency of PA = Peano Arithmetic. I was never impressed by this objection, which has largely disappeared from modern discussion (that I see) nowadays. I never believed that there was a sufficiently clear informal notion of "extended finitism" that would admit a definitive analysis. So my view was that for Hilbert's program, one needs to point to a particular formalization of a particular kind of reasoning R, and point to a particular formalization T of a particular kind of or area of mathematics, and then investigate whether R is sufficient to prove the consistency of T. The general pattern of findings along these lines are now very well known. Godel's second incompleteness theorem is of the utmost relevance, with devastating effects. This comes about in the following way. The general approach to formalizations R and to formalizations T are similar, where very frequently R is a fragment of T, or at least (usually trivially) interpretable in T in the sense of Tarski. GODEL (modified for this purpose). If R is interpretable in T and T is reasonable, then R does not prove the consistency of T. More specifically, there is a system PRA (primitive recursive arithmetic) that some authors like to identify with Hilbertian finitism. In all of the proposed formalizations of extensive mathematics - including, say, what goes on in such things as FLT - there is more than enough to easily interpret PRA. So by Godel, Hilbert's program cannot be carried out in such a setup. There has been considerable progress on one front. Namely, to show that a lot of interesting mathematics can be proved consistent within PRA. Perhaps most notably, the consistency of Elementary Algebra and Geometry - formalized by, say, real closed fields - is proved consistent in PRA, and even in the much much weaker system EFA (exponential function arithmetic, or ISigma(exp) discussed in, say, Hajek/Pudlak). See posting #56. In fact, RCF (real closed fields) is interpretable in Robinson's Q (interpretable in the sense of Tarski). Hence RCF is consistent relative to Q in an appropriate sense. The other direction is false (for interpretability and relative consistency), so that in some sense RCF is weaker than Q! And this despite the fact that RCF is about a continuous context, yet Q is about a discrete context. The interesting thing about this is the use of weak fragments of arithmetic to prove the consistency of continuous reasoning (although it is fundamentally algebraic reasoning). There is an expectation of continuing this program to cover much more continuous mathematics - perhaps continuous mathematics that is not fundamentally algebraic in nature. But this is still a rather weak, mild, restrained resurrection of Hilbert's program. There is no expectation that one will be able to prove consistency of mathematical reasoning that involves, say, the kind of discrete mathematical objects used in the consistency proofs. E.g., iterated exponential functions on the positive integers, to say nothing about general discrete functions, or Borel measurable sets of real numbers, or even unrestricted sets of real numbers. After all, there is Godel's second incompleteness theorem to contend with. Or is there? 2. FIRST PROBLEM ABOUT PUBLISHED NUMBER THEORY. Let us consider what happens when we formalize a kind of or area of mathematics. In the case of PA and arithemtic reasoning, the modern way of looking at it is to observe that induction is used over and over again throughout arithmetic reasoning, and also every other type of arithmetic reasoning - e.g., pigeonhole, counting arguments, etcetera, are easily reduced to induction. One also remarks that if you do arithmetic reasoning, you are in the mindset to accept induction for any arithmetic property. It is acknowledged that maybe there is something more basic about induction with respect to properties that don't need quantifiers, but it is natural to use quantifiers in many contexts, and there is no reason to accept induction with respect to some arithmetic formulas with quantifiers and not for all arithmetic formulas with quantifiers. So people look at all of PA. And obviously by Godel, PRA does not prove the consistency of PA. However: *it is clear that mathematicians do not apply induction with respect to arbitrary arithmetic formulas. * In one sense, this is a complete triviality. There are only finitely many people who have ever lived, and each one of them uses only finitely many arithmetic formulas for induction in their lifetime of arithmetic reasoning. But *maybe mathematicians only apply induction with respect to arithmetic formulas that have some as yet undisclosed special property.* We would know exactly what to do about this situation if we knew the as yet undisclosed special property that the arithmeitc formulas to which induction is actually applied to. We would then make the appopriate formalization of the appropriate fragment of PA and then decide whether or not the resulting system can be proved consistent within PRA, or even within EFA. In fact, for celebrated published number theory, such a study has already been proposed. Namely, QUESTION 1: Is every published theorem in number theory, conveniently stated in the language of first order arithemtic (possibly with conventional coding apparatus), provable in EFA (exponential function arithemtic or ISigma0(exp))? So in this study, the special property is that only bounded quantification is involved, with the help of exponentiation (beyond the ring structure of the integers). If this is the case, then clearly published number theory is provably consistent within PRA, or even weaker systems that prove the consistency of EFA. E.g., EFA* = superexponential function arithmetic or ISigma0(superexp). See Hajek/Pudlak. 3. DISCUSSION OF MODELS OF LOGICAL REASONING. However, can published number theory be proved consistent within EFA? The immediate answer of no, using the result of Wilkie/Paris that EFA does not even suffice to prove the consistency of Robinson's Q, and Robinson's Q is obviously part of published number theory. However, we can go further, and become more critical: *it is clear that mathematicians do not apply first order reasoning with respect to arbitrary logical formulas.* And once again, in sone sense, this is a complete triviality. There are only finitely many people who have ever lived, and each one of them uses only finitely many logical formulas in their lifetime of reasoning. But again *maybe mathematicians only reason with respect to logical formulas that have some as yet undisclosed special property.* And again: we would know exactly what to do about this situation if we knew the as yet undisclosed special property that the logical formulas actually used have. We would then make the appopriate formalization of the appropriate fragment of predicate calculus and then decide whether or not the resulting systems can be proved consistent within various systems. We will not go further with this line of reasoning - which leads to a whole new set of issues and programs. In particular, in this posting, we will consider the unrestricted use of first order predicate calculus as given; i.e., an assume part of any model of mathematical reasoning that we are trying to prove consistent - or trying to prove cannot be proved to be consistent. But we leave this matter with a few remarks. It makes perfectly good sense to restrict predicate calculus along various lines. However, when examining the use of predicate calculus reasoning in mathematics, one needs to bear in mind that it is, in a literal sense, both too large and too small. In particular, it is too small in that the usual formalizations do not accomodate abbreviations, and mathematics simply cannot be done without abbreviations. So whereas it is true that mathematicians do not consider very many logical formulas, they do make lots of abbreviations, which allows them to manipulate complex formulas implicitly in terms of long series of small formulas. This is an essential aspect of mathematics. One can of course go even further and consider finite models of mathematical reasoning, whereby there is a bound placed on the size of any proof. And then consider what systems can prove consistency in this sense - but with restricted size. This leads to the finite Godel's theorem, and my initial work on this was extended by Pudlak and reported in the Handbook of Proof Theory. But this whole matter leads to another set of subtle issues that is outside the scope of this posting. Of course, one can take this to the extreme of the extreme, and criticize any model of mathematical reasoning whatsoever, and claim that mathematics has no significant logical patterns - or at least none that can be appropriately circumscribed. That the Hilbert program can only amount to checking that there is no published proof in the literature of an inconsistency!! Of course this is easily done, so in this sense consistency is easily proved. However, this is not a good model of mathematical reasoning - i.e., presence in the already published literature. Because the next time someone publishes something, it will not be covered in the model. For the rest of this posting, we will take first order predicate calculus with equality (fopce) for granted. This can be replaced by a finite fragment of fopce - where there are only finitely many well formed formulas, up to change of symbols - with abbreviation power. Exactly what finite fragment is needed, required, suitable, or convenient - is an interesting and important question. 4. MORE PROBLEMS ABOUT PUBLISHED NUMBER THEORY. So what is the status of the consistency of published number theory? PROBLEM 2. Is it provable in EFA that the consistency of published number theory implies the consistency of EFA? By combining problems 1 and 2, we get PROBLEM 3. Is it provable in EFA that the consistency of published number theory is equivalent to the consistency of EFA? It is known that *it is not provable in EFA that the consistency of Q implies the consistency of EFA.* *it is not provable in EFA that the consistency of ISigma0 (polynomially bounded arithmetic) implies the consistency of EFA.* We proved that *it is not provable in EFA that the consistency of RCF (real closed fields) implies the consistency of EFA.* PROBLEM 4. Does published number theory imply EFA = ISigma0(exp)? Or even just ISigma0? PROBLEM 5. Does published number theory imply the consistency of EFA = ISigma0(exp)? To get the ball rolling, I am working on some "friendly" number theoretic facts which not only imply EFA and the consistency of EFA, they are equivalent to EFA, ISigma1, and ISIGMA2. That is - if these "friendly" number theoretic facts are counted as published number theory. But it is most interesting to do this under a strict interpretation of "published number theory", and I can't say that these examples are that good yet. 5. A CONCRETE EXAMPLE. There are zillions of them. For example, consider T = the set of all statements in Hardy/Wright that are trivially formalizable in the language of discrete ordered rings, and T' = the set of all statements in Hardy/Wright that are trivially formalizable in the language of discrete ordered rings with exponentiation on the positive integers. What is the logical status of T and T'? Naturally, we view the axioms of discrete ordered rings (i.e., the integers form a discrete ordered ring) as part of T and T', and also the various Tarski laws of exponentiation as part of T'. Here is just one concrete example to focus attention on. Look at the axioms: Z is a discrete ordered ring, plus the four squares theorem (every positive integer is the sum of four squares). What is the logical status of this system? And consider the following system. 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. What is the logical status of this system? Is it equivalent to ISigma0(factorial), which would make it bi-interpretable with EFA? Does it make any difference if we strengthen 6 to FLT, with suitable Tarski axioms for exponentiation? 6. DISCRETE MATHEMATICS. Discrete mathematics is "wilder" than number theory. It should be quite easy to see that published discrete mathematics has high logical strength, at least significantly higher than EFA. After all, there is celebrated discrete mathematics that demonstrably involves very fast growing functions and large integers - e.g., Ackerman. So this should be easy. Wrong. For example, let us take what should be an easy case. Ramsey's theorem for n-tuples for infinite sets of natural numbers. In reverse mathematics over the base theory RCA0, this implies ACA0 and is in fact a bit stronger (discussed in Simpson's book). But what about without the base theory? It is easier to talk about formalization in the special case of n = 3 where in the reverse mathematics setup, this is equivalent to ACA0. What one needs is some principles of discrete mathematics to get enough induction or induction like principles and enough power to get some recursion theoretically serious infinite sets of natural numbers. It is not clear how to do this appropriately, starting from scratch, and staying within published discrete mathematics. 7. OF COURSE IT CAN BE DONE (SORT OF). Of course one can generate consistency strength in some reasonable ways. But every time I start to write something reasonable down, I am shocked by how much more striking it would be to do it in some other ways that literally quote from celebrated theorems in the literature. And there are so many possibilities for doing this that cannot be dismissed out of hand - that just might work. That is where the excitement is. On the other hand, it is now clear from many examples that genuine metamathematical phenomena studied intensively in f.o.m. has been shown to be quite well embedded in mathematics - at least through fast growth rates and large integers. E.g., see postings #19, #21, #22, #24, #25, #27, #34, #36, #37, #40, #42, #43, #50, #51, #69, #71. And this is the case despite the fact that in order to generate consistency strength in these examples, one needs a kind of logician's base theory going well beyond what is in the published literature. A reasonable stab at generating consistency strength from mathematical facts was presented in #46. And I intend to present others. Does strict adherence to celebrated theorems in the literature lead to substantial consistency strength or not? That is the intriguing question. ********** This is the 73rd 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

**Follow-Ups**:**Stephen G Simpson**- FOM: Hilbert's program and RCF

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

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