FOM: 76:Finite set theories
Harvey Friedman
friedman at math.ohio-state.edu
Tue Dec 28 13:28:52 EST 1999
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
More information about the FOM
mailing list