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

*To*: fom@math.psu.edu*Subject*: FOM: 76:Finite set theories*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Tue, 28 Dec 1999 13:28:52 -0500*Sender*: owner-fom@math.psu.edu

Many weak subsystems of arithmetic correspond to weak systems of finite set theory. Also the systems of finite reverse mathematics being proposed correspond to weak systems of finite set theory. It may turn out to be a good idea to use these finite set theories as the basic formal systems of finite reverse mathematics instead of just having nonnegative integers and finite sets of nonnegative integers as was proposed in posting #75. The proposals in posting #75 just use nonnegative integers and finite sets of nonnegative integers, and then rely on coding for other finite objects. It's just too early to tell. However, one thing is clear. Moving over to finite set theories is not a good idea for the purposes of the delicate issue addressed in section 1 of posting #75 (and also posting #73). For this we want to be as minimalistic as possible - conforming to what mathematicians view as minimalistic, not set theorists. 1. BACKGROUND ON INTERPRETABILITY. We will be referring to Petr Hajek, and Pavel Pudlak, Metamathematics of First-Order Arithmetic, 1998, Springer. in this section. Although it is not known whether ISigma_0 = BA = bounded arithmetic, is finitely axiomatizable (it is suspected not to be), it is known that it is interpretable in some very weak fragments of itself. In particular, after initial results by Nelson, Wilkie proved that ISigma_0 is interpretable in the fragment Q, whose language is 0,S,+,*,<=,=, and whose axioms are: 1. Sx not= 0. 2. Sx = Sy implies x = y. 3. x not= 0 implies (therexists y)(x = S(y)). 4. x+0 = x. 5. x+Sy = S(x+y). 6. x*0 = 0. 7. x*Sy = x*y + x. 8. x <= y iff (therexists z)(z+x = y). In posting12/23/99 8:24AM I gave some necessary and sufficient conditions for interpretabilty in Q. They apply to FCA, and so FCA is interpretable in Q. In a footnote on page 366, Hajek/Pudlak remark (no attribution) that Q is interpretable in the following extremely weak fragment of ZFC in the language epsilon,=: 1. (therexists x)(forall y)(not y epsilon x). 2. (therexists z)(forall w)(w epsilon z if and only if (w = x or w epsilon x)). And it can be proved in various ways that this system is interpretable in Q. Of course, these are interesting and important theoretical results about interpretability, and the interpretability relation is of fundamental importanc. Of course, the interpretations are horrifically complicated and useless in actual formalization. In this particular posting, we are interested in interpretations that meet some additional criteria. 2. SET THEORIES CORRESPONDING TO ISigma_0 AND FCA. Recall the system FCA of posting #75, section 2, which is a proposed base theory for finite reverse mathematics. It is a conservative extension of ISigma_0 which has axioms for finite sets of nonnegative integers. And it has strictly mathematical axiomatizations according to posting #75, section 1. We will endeavor to make our set theories conform to the usual axioms of ZFC, in order to facilitate comparison. We start with the following fairly standard formulation of ZF in the language epsilon,=. 1. Extensionality. 2. Pairing. 3. Union. 4. Foundation. 5. Separation. 6. Choice. 7. Power set. 8. Replacement. 9. Infinity. We saw in section 1 that extremely weak set theories are sufficient to interpret ISigma_0. However, here we will be interested only in interpretations of fragments of arithmetic where the nonnegative integers get interpreted as von Neumann ordinals, 0 as the empty set, S as successor in the ordinals, and < as epsilon on the ordinals. Then the natural subsystem of ZF to take in order to interpret ISigma_0, and hence FCA, is as follows. 1. Extensionality. 2. Pairing. 3. Union. 4. Foundation'. Every nonempty set has an epsilon minimal and an epsilon maximal element. 5. Bounded separation. Separation for bounded formulas. 6. Enumeration. Every set is in one-one correspondence with an ordinal. 7. Cartesian product. The set of all ordered pairs from any set is a set. This system also interprets FCA, where finite sets of nonnegative integers get interpreted as sets of ordinals. In addition, there is an interpretation of this system in ISigma_0, and hence in Q. We can also add 8. Transitive closure. There is a least set containing all elements of any given set. More can be said. The obvious interpretation of addition by x+y = z if and only if x dot {emptyset} union y dot {{emptyset}} is in one-one correspondence with z, and of multiplication by x*y = z if and only if x dot y is in one-one correspondence with z, works, and in fact provides a faithful interpretation of ISigma_0 in this system (with or without trnansitive closure). In addition, there is an interpretation of this system, with transitive closure, in Q. We also obtain a faithful interpretation of FCA in this system (with or without transitive closure) in this way, by interpreting sets of nonnegative integers as sets of ordinals. 3. SET THEORIES CORRESPONDING TO ISigma_0(exp) = EFA, AND FPS. Recall the system FPS of posting #75, section 5, which is a proposed principle system for finite reverse mathematics extending the proposed base theory FCA. It is a conservative extension of ISigma_0(exp) = EFA which has axioms for finite sets of nonnegative integers. And it has strictly mathematical axiomatizations according to posting #75, section 1. The analogous system to section 2 is obtained by replacing Cartesian product with power set: 1. Extensionality. 2. Pairing. 3. Union. 4. Foundation'. Every nonempty set has an epsilon minimal and an epsilon maximal element. 5. Bounded separation. Separation for bounded formulas. 6. Enumeration. Every set is in one-one correspondence with an ordinal. 7. Power set. And again we can optionally add 8. Transitive closure. There is a least set containing all elements of any given set. The analogous results to section 1 hold with ISigma_0 replaced by ISigma_0(exp) = EFA, and with FCA replaced by FPS. 4. SET THEORIES CORRESPONDING TO ISigma_0(superexp) = EFA, AND FIPS. Recall the system FIPS of posting #75, section 6, which is a proposed principle system for finite reverse mathematics extending the proposed base theory FCA, and extending FPS. It is a conservative extension of ISigma_0(superexp) which has axioms for finite sets of nonnegative integers. And it has strictly mathematical axiomatizations according to posting #75, section 1, where, e.g., the full finite Ramsey theorem is added. The analogous system to sections 2 and 3 is: 1. Extensionality. 2. Pairing. 3. Union. 4. Foundation'. Every nonempty set has an epsilon minimal and an epsilon maximal element. 5. Bounded separation. Separation for bounded formulas. 6. Enumeration. Every set is in one-one correspondence with an ordinal. 7. Cumulation. The cumulative hierarchy exists on every ordinal. We can optionally add 8. Exhaustive cumulation. The cumulative hierarchy exists on every ordinal and exhausts every set. in which case we can omit union and eumeration and cumulation, as they are derivable. This results in the system: 1. Extensionality. 2. Pairing. 3. Foundation'. Every nonempty set has an epsilon minimal and an epsilon maximal element. 4. Bounded separation. Separation for bounded formulas. 5. Exhaustive cumulation. The cumulative hierarchy exists on every ordinal and exhausts every set. The analogous results to section 1 hold with ISigma_0 replaced by ISigma_0(superexp), and with FCA replaced by FIPS. ********** This is the 76th 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 74:Reverse arithmetic beginnings 12/22/99 8:33AM 75:Finite Reverse Mathematics 12/28/99 1:21PM

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

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