FOM: 90:Two Universes
Harvey Friedman
friedman at math.ohio-state.edu
Fri Jun 23 13:34:09 EDT 2000
This posting concerns some improvements on paper [1], which is the first in
a series of three papers.
[1] The axiomatization of set theory by extensionality, separation, and
reducibility, October 28, 1997.
[2] The interpretation of set theory in mathematical predication theory,
October 25, 1997.
[3] The interpretation of set theory in pure predication theory, August 20,
1997.
You can find these papers at
http://www.math.ohio-state.edu/foundations/manuscripts.html
These papers contain detailed proofs of a great number of results, and I
won't summarize them all here. I will, however, mention one result from [1]
that gives a new axiomatization of ZF\foundation, and a second result from
[1] that gives a new axiomatization of at least arbitrarily large
measurable cardinals.
But before doing this in sections 2 and 3, we will give some philosophical
motivation behind the two universe approach.
1. The Two Universe Approach.
Actually, we have also considered more than two universes, but for most
results only two universes are used.
The idea is this. The first universe is created on the first day. The
second universe is created on the second day by reflecting on the first
universe. Via Russell's paradox, one can introduce new objects for the
second universe. This is relevant to sections 2,3 below, but not clearly
relevant to section 4 below.
The first universe is always represented by the constant (or unary
predicate) W. The second universe is represented by the fact that variables
always range over the second universe - which is the full universe in a two
universe theory.
Since W represents a full, completed, universe - whatever that means - it
must be the case that the extension to the second universe is, in some
sense, an inessential extension. It must resemble the first universe.
This general framework is sufficient to give some reasonable motivation for
a number of systems, which prove to be surprisingly powerful.
2. ZF.
Let L(epsilon,W) be the classical first order predicate calculus based on
the binary relation symbol epsilon and the constant symbol W, with the
usual axioms and rules of inference. Let K(W) be the theory in L(epsilon,W)
given by the following axioms. (Here we use "in" for epsilon).
i. Extensionality. (forall z)(z in x iff z in y) implies (forall z)(x in z
iff y in z).
ii. Witenessing.. x_1,...,x_n in W & (therexists y)(phi) implies
(therexists y in W)(phi), where n >= 0 and phi is any formula in L(epsilon)
whose free variables are among the distinct variables x_1,...,x_n,y.
iii. W Separation. x in W implies (therexists y in W)(forall z)(z in y iff
(z in x & phi)), where phi is any formula in L(epsilon,W) in which y is not
free.
The names of ii and iii differ from those used in [1],[2],[3].
It is shown in [1] that this system corresponds closely to ZF in various
precise senses. For instance, the theorems of this system that don't
mention W are exactly the theorems of ZF\foundation, where the reflection
axiom scheme is used instead of replacement (in the presence of foundation,
they are equivalent).
In [2], we showed that the system based on ii and iii only (with i dropped)
also corresponds to ZF in a precise sense. Thus we have an interpretation
of ZFC using just the two axioms:
Witnessing, W Separation.
This result extends very naturally to three and more universes, where we
get the subtle cardinal hierarchy. But for cardinals breaking L, we use
another idea.
3. Measurable cardinals.
i. Extensionality. (forall z)(z in x iff z in y) implies (forall z)(x in z
iff y in z).
ii. Witnessing. (x_1,...,x_n in W & phi) implies (therexists y in W)(phi),
where n >= 0 and phi is any formula in L(epsilon) whose free variables are
among the distinct variables x_1,...,x_n,y.
iii. Largest Transitive Set. (therexists x in W)(forall transitive y
containedin W)(y containedin x).
iv. Relative W Separation. x in W implies (therexists y in W)(forall z in
W)(z in y iff (z in x & phi)), where phi is any formula in L(epsilon,W) in
which y is not free.
In [1], it is shown that in Extensionality, Witnessing, and W Separation,
we can prove that W is transitive and W is not in W. THerefore, in
Extensionality, Witnessing, and W separation, we can refute Largest
Transitive Set. This is why we use Relative W Separation here instead of W
Separation.
The names of iii and iv differ from those used in [1],[2],[3]. In [1], we
proved that this system interprets (in fact, proves the consistency of) ZF
+ "there exists rbitrarily large measureable cardinals" and is
interpretable in (in fact, its consistency is provable in) "there is a
nontrivial elementary embedding from a rank into a rank" - not a rank into
itself, which is of course much stronger. The results can also be stated in
terms of epsilon models.
We have not gone back into the issue of dropping extensionality because of
lack of time, but we are morally certain that we can do this in the same
way that it was carried out in detail in [2] as described in section 2
above. Thus we would get an interpretation of ZFC + "arbitrarily large
measurable cardinals" using just the three axioms:
Witnessing, Largest Transitive Set, Relative W Separation.
4. Rank into itself.
In [1], we went on to higher cardinals, with somewhat more involved axioms.
Here we present a system which is only slightly more complicated than in 3
above, but which already goes to ZF + j:V(alpha) into V(alpha).
This time we use the language L(epsilon,W), where W is a *predicate*
symbol. We use "x in W" as an abbreviation for W(x).
i. Extensionality. (forall z)(z in x iff z in y) implies (forall z)(x in z
iff y in z).
ii. Witnessing. (x_1,...,x_n in W & (therexists y)(phi)) implies
(therexists y in W)(phi), where n >= 0 and phi is any formula in L(epsilon)
whose free variables are among the distinct variables x_1,...,x_n,y.
iii. Largest Transitive Set. (therexists x in W)(forall y containedin W)(y
transitive implies y containedin x).
iv. Relative W Replacement. (forall y in x)(therexistsunique z)(phi)
implies (therexists w in W)(forall z in W)(z in w iff (therexists y in
x)(phi)), where phi is any formula in L(epsilon,W) in which w is not free.
Since we don't have equality, uniqueness in iv is formulated in terms of
extensional equality.
This theory interprets (in fact, proves the consistency of) ZF + "there is
a nontrivial elementary embedding from some V(alpha) into V(alpha)" and is
interpretable in (in fact, its consistency is provable in) ZF + "there is a
nontrivial elementary embedding from some V(alpha+1) into V(alpha+1)". The
results can also be stated in terms of epsilon models.
It seems likely that we can carry over the dropping extensionality
technique to get an interpretation of ZF + "there exists a nontrivial
elementary embedding from some V(alpha) into V(alpha)" using just the three
axioms:
Witnessing, Largest Transitive Set, Relative W Replacement.
5. Measurable Cardinals Again.
We can also redo section 3 using W as a predicate symbol instead of a
constant symbol. We still take the same presentation, only with W as a
predicate symbol:
i. Extensionality. (forall z)(z in x iff z in y) implies (forall z)(x in z
iff y in z).
ii. Witnessing. (x_1,...,x_n in W & phi) implies (therexists y in W)(phi),
where n >= 0 and phi is any formula in L(epsilon) whose free variables are
among the distinct variables x_1,...,x_n,y.
iii. Largest Transitive Set. (therexists x in W)(forall transitive y
containedin W)(y containedin x).
iv. Relative W Separation. x in W implies (therexists y in W)(forall z in
W)(z in y iff (z in x & phi)), where phi is any formula in L(epsilon,W) in
which y is not free.
We get the same results as in section 3.
****************************
This is the 89th 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
More information about the FOM
mailing list