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

*To*: fom@math.psu.edu*Subject*: FOM: 46:Tamism*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Wed, 14 Jul 1999 11:25:20 +0100*Sender*: owner-fom@math.psu.edu

This is the 46th 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 1. TAMISM Number theory, finite algebra, and finite combinatorics provide a wealth of theorems that could be subject to the reverse mathematics idea but which are readily provable in RCA_0 and so cannot be analyzed under the present framework. Incidentally, this remark is believed to apply to many modern developments; e.g., we expect that the Faltings and Wiles theorems can be proved in RCA_0, but nobody seems to have verified this. Basically, there is almost no reverse mathematics of arithmetical sentences from standard mathematics. [There are Kruskal and related theorems, and the new 1998 ³perfect² finite forms - another story for another day.] We attack this by proposing reverse *arithmetic*. This involves a reduction (or alteration) of the primitives, weakening of the axioms, and a restricting (or refocusing) of the subject matter analyzed. This is discussed in my talk at the Boulder meeting; there will be a paper for its Proceedings. In this posting, I will confine myself to what I call **severe** reverse arithmetic** and a doctrine I call "tamism." An interesting and devastating suggestion is: "that meta-mathematical phenomena uncovered by reverse math is an artifact of choice of base theory; the base theory injects a math logic slant that is foreign to the spirit of math; the present way of formalizing math is not sufficiently tied to the math itself so that mathematically irrelevant issues come up such as what formulas should induction be applied to; the base theory does not consist entirely of "essential" math; math might be formalized in a more subtle and relevant way so that a consistency proof can be given in weak fragments of arithmetic such as EFA (exponential function arithmetic)." We call this interesting position "tamism". The case for tamism is bolstered by the success of the program of creating so called "tame" systems which formalize much important math in a quite different way, which do allow consistency proofs of the kind that Hilbert envisioned. Two of the most famous examples are that of Presburger arithmetic and real closed fields. By the way, I am involved in the tame systems and structures program (some aspects jointly with Chris Miller). NOTE: I now claim that the metamathematics of real closed fields can be carried out in EFA, including a consistency proof. See forthcoming posting. Tamism in the extreme would contend that all (interesting) mathematics can be cast in a single demonstrably consistent tame system, thus skirting virtually the entire mainline development of mathematical logic of the 20th century, and in particular reverse mathematics as currently practiced. It is imperative that we look for absolute refutation of tamism that leave no wiggle room. DOWN WITH TAMISM!! In an embodiment of reverse mathematics, the level of necessity of the mathematics formalized in the base theory is what we call its ³severity². Current reverse mathematics is distinctly not severe on the choice of axioms for the base theory RCA_0. My original formulation of the axioms for RCA_0 is considerably more severe than the logically equivalent formulation in Simpson¹s book. Simpsonís presentation is of course more convenient. However, even my original axioms for RCA_0 are not severe enough. There is always wiggle room about what is absolutely essential about infinitary objects. And the severity level of the choice of theorems analyzed in reverse mathematics is also subject to wiggle room; e.g., "arbitrary continuous functions on I are too general for modern mathematics?!" So for an absolute refutation of tamism, we look to finite mathematics - especially number theory and finite combinatorics. 2. REFUTING TAMISM. SEVERE REVERSE ARITHMETIC The base theory for severe reverse arithmetic will be the axioms of discrete ordered (commutative) rings (with unit) in the language 0,1,+,-,mult,=,<. NOTE: In order to develop a smooth theory of reverse arithemetic - as opposed to **severe** reverse arithmetic - we may well need a somewhat bigger base theory. It took some time for it to be clear that my RCA_0 was the "right" base theory for the present (first) incarnation of reverse mathematics. It's not too strong and not too weak. Further incarnations of reverse mathematics will involve weaker base theories (or base theories with different primitives). Similarly, the "right" base theory for the first incarnation of reverse arithmetic - not too strong and not too weak - will take some experimentation. This matter will be discussed in the Proceedings of the Boulder meeting. We are going to refer to EFA (exponential function arithmetic) as a benchmark, with 0,S,+,mult,=,<, base 2 exp, successor axioms, defining equations, definition of <, and induction with respect to all bounded formulas in the language. EFA can easily be reformulated in the context of discrete ordered rings. We need to find some essential facts about the integers (and associated finite objects) - universally respected and loved - which when added to the axioms of discrete ordered rings imply EFA. With EFA in hand, we can go further in many directions to get even stronger systems, burying tamism further. 1. Axioms for the discrete ordered ring, (Z,0,1,+,-,mult,=,<). 2. Axioms for vectors of finite length from Z, equality, length, and picking out coordinates: Every integer is a vector of length 1. Vectors of the same length are equal if and only if their coordinates are equal. There is a zero vector of every length. Vectors of the same length can be added, substracted, and multiplied by scalars. We can append any integer to any vector and obtain a vector of one higher length. We can delete the last coordinate of any vector of length > 1 and obtain a vector of one smaller length. We can change any coordinate of any vector and obtain a vector of the same length. 3. Axioms for linear transformations from vectors of one length into vectors of another length: The constantly zero functions are linear transformations. Linear transformations of the same dimensions can be added and subtracted. Linear transformations can be multiplied by scalars. Linear transformations with matching dimensions can be composed. For any linear transformation, there is a unique linear transformation which agrees with it at all unit basis vectors except one, where its value is reassigned. 4. Axioms for finite sets of vectors, all of the same dimension: Every singleton is a finite set of vectors. Finite sets of vectors are closed under pairwise union, pairwise intersection, set theoretic difference, and Cartesian product. The translation by a vector of any finite set of vectors is a finite set of vectors. 5. Axioms for the unit basis vectors: Every finite set of vectors in a given dimension is the forward image of the set of unit basis vectors in some dimension under a linear transformation on that dimension. The forward image of the set of unit basis vectors under a linear transformation is a finite set of vectors. (NOTE: This forward image is the set of rows in the matrix of the linear transformation). 6. Any finite set of nonzero integers has a common multiple. 7. For all integers n >= 1, {k: 1 <= k <= n} and {k^2: 1 <= k <= n} exist as finite sets. 8. Every nonempty finite set of integers has a least element. THEOREM 1. EFA and 1-8 are interpretable in each other, and prove the same sentences in the language of ordered rings. Dimitracopoulos has proved the MRDP theorem in EFA, and this allows some nice simple additions to 1-8 that climb up to Simga_1 induction. E.g., 9. Axioms for polynomnials (as funtions) from vectors of a fixed length into integers. Constant and projection functions are polynomials. Polynomials can be added, substracted, and multiplied. 10. Every polynomial takes on a value of least magnitude. THEOREM 2. Sigma_1 induction and 1-10 are interpretable in each other, and prove the same sentences in the language of ordered rings. There are much simpler ways to extend the discrete ordered ring axioms to get strength if we are willing to be less severe. This is discussed in my talk at the Boulder meeting, June 13-17, 1999. It will be posted on my website soon, and there will be a manuscript submitted for the conference proceedings.

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

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