FOM: 97:Classification of Set Theories
Harvey Friedman
friedman at math.ohio-state.edu
Fri Dec 22 07:55:05 EST 2000
In posting #96, Comments on BRT, I wrote:
>This is an infinite disjoint cover theorem. One asks for a bi-infinite
>disjoint cover theorem. After a succession of attempts with
>counterexamples, one is inexorably led to the theorem
>
>"Let f,g be strictly dominating integral multivariate functions. There
>exists bi-infinite A containedin B containedin Z such that fA is disjointly
>covered by B,gB, and fB is disjointly covered by C,gC."
This should read:
>This is an infinite disjoint cover theorem. One asks for a bi-infinite
>disjoint cover theorem. After a succession of attempts with
>counterexamples, one is inexorably led to the theorem
>
>"Let f,g be strictly dominating integral multivariate functions. There
>exists bi-infinite A containedin B containedin Z such that fA is disjointly
>covered by B,gB."
Also, my ... came out as S on some computers and in the Archives:
A_1,S,A_m
f_1A_1,S,f_1A_m
S
f_nA_1,S,f_nA_m.
This should read
A_1,...,,A_m
f_1A_1,...,,f_1A_m
...
f_nA_1,...,f_nA_m.
######################
CHARACTERIZATION OF SET THEORIES
December 22, 2000
A longstanding goal has been to show that set theory, including ZFC and ZFC
+ large cardinals, is in some sense inevitable, at least in the sense that
"there is only one way to go up".
At least
"there is only one way to go up, up to mutual interpretability".
We present an approach to this problem, at least for quite a ways up. To be
precise, through the subtle cardinal hierarchy.
In the treatment here, we assume that we have universes represented by
constant symbols Vn, n >= 1. We put down axioms that commit ourselves to an
appropriate form of separation. This theory, T0, is in the language of
first order predicate calculus based on epsilon,=, and the constant symbols.
1. Extensionality. Any two sets with the same elements are =.
2. Separation for the Vn. The set of all elements of any given element of
Vn satisfying any formula with parameters, lies in Vn.
Note that T0 is quite weak. Let alpha_1,alph_2,... < beta be any ordinals,
perhaps finite. We can take Vn = V(alpha_n), and the universe = V(beta),
with epilson interpreted as membership.
We can think of T0 as announcing that we are doing a basic style of set
theory with infinitely many universes, all inside a universe.
There are other conceptions of multi universe set theory which we have used
in connection with measureable cardinals and beyond, based on a weaker
restricted separation. See, e.g., #90, #97. But this is the simplest one to
work with for present purposes.
I am fairly sure from past experience that the Extensionality axiom can be
dropped, and the results will still hold. In particular, see Theorem 1.
For our results, we need a little general theory of schemes in predicate
calculus; in particuar, the distinction between pure and general schemes.
DIGRESSION ON GENERAL THEORY OF SCHEMES.
Let L be ordinary first order predicate calculus based on a language, which
may or may not include equality. To implement schemes, we add infinitely
many Greek letters of each arity, which will be treated as predicate
symbols.
A scheme is simply any formula in this extended language.
We now make the key definition that tells us what a (general) substitution
instance of a scheme is. These will be certain formulas of L (without Greek
letters).
Let PHI be a scheme. To make a substitution instance of PHI, we assign to
each Greek letter alpha in PHI, a formula phi of L (no Greek letters),
which to be safe, does not have any variables in common with PHI. Also k
distinct variables y1,...,yk are listed, again not appearing in PHI, where
k is the arity of the Greek letter, and where y1,...,yk are not bound
variables in phi. Here y1,...,yk are is called the substituting variables
list.
The substitution is effected as follows. For each atomic formula
alpha(t1,...,tk) in PHI, where alpha is one of the Greek letters, we
replace alpha(t1,...,tk) by phi(y1/t1,...,yk/tk), where phi has been
assigned to alpha.
This is general subsitution (general subsitution instances) because we make
no restriction on the number of free variables in phi.
In restricted subsitution (restricted subsitution instances), we will also
prepare a list associated with each Greek letter alpha appearing in PHI.
This list tells us
i) which constant symbols, relation symbols, and function symbols, called
the side symbols, that are allowed to be present in the formulas phi that
can be assigned to alpha for the purpose of substitution;
ii) which variables, called the side variables, other than those in the
substituting variables list, are allowed to be free in the formulas phi
that can be assigned to alpha for the purpose of substitution (they never
include any variables in PHI).
One can be more general about this, and go into these matters in greater
detail. But this suffices for our purposes.
We will need to use restricted subsitution below.
END OF DIGRESSION.
We now consider all restricted schemes for the language of T0 that are
quantifier free, and where, in any atomic formula that occurs, no variable
appears to the right of epsilon. We call such a scheme *structural*.
The schemes shown in Theorem 1, one for each p >= 1, are examples of
structural schemes.
Let SUB = ZFC + {there exists an n-subtle cardinal}_n.
THEOREM 1. Consider T0 together with the schemes: x in V1 implies
(phi(x,V1,...,Vp) iff phi(x,V2,...,Vp+1)), where substitution is restricted
so that there are no side variables, and no side constant symbols (epsilon
is of course a side symbol). Then T0 is mutually interpretable and
equiconsistent with SUB.
THEOREM 2. Let K be T0 together with any set of structural schemes. Then K
is inconsistent or interpretable into SUB. If K has finitely many structual
schemes then K is inconsistent or provably consistent within SUB. Every
such K is interpretable into a finite subset of SUB, and every finite
subset of SUB is interpretable into such a K.
****************************
This is the 97th 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
76: Finite set theories 12/28/99 1:28PM
77:Missing axiom/atonement 1/4/00 3:51PM
78:Qadratic Axioms/Literature Conjectures 1/7/00 11:51AM
79:Axioms for geometry 1/10/00 12:08PM
80.Boolean Relation Theory 3/10/00 9:41AM
81:Finite Distribution 3/13/00 1:44AM
82:Simplified Boolean Relation Theory 3/15/00 9:23AM
83:Tame Boolean Relation Theory 3/20/00 2:19AM
84:BRT/First Major Classification 3/27/00 4:04AM
85:General Framework/BRT 3/29/00 12:58AM
86:Invariant Subspace Problem/fA not= U 3/29/00 9:37AM
87:Programs in Naturalism 5/15/00 2:57AM
88:Boolean Relation Theory 6/8/00 10:40AM
89:Model Theoretic Interpretations of Set Theory 6/14/00 10:28AM
90:Two Universes 6/23/00 1:34PM
91:Counting Theorems 6/24/00 8:22PM
92:Thin Set Theorem 6/25/00 5:42AM
93:Orderings on Formulas 9/18/00 3:46AM
94:Relative Completeness 9/19/00 4:20AM
95:Boolean Relation Theory III 12/19/00 7:29PM
96:Comments on BRT 12/20/00 9:20AM
More information about the FOM
mailing list