[FOM] 444: The Exploding Universe 1
Harvey Friedman
friedman.8 at asc.ohio-state.edu
Mon Nov 1 01:46:40 EDT 2010
THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION
*****************************************
We have previously developed a foundations of ZF and large cardinals
via two set theoretic universes. See
The Axiomatiation of Set Theory by Extensionality, separation, and
Reducibility, http://www.math.ohio-state.edu/%7Efriedman/manuscripts.html
section 1, #13, October 28, 1997.
Here we generate large cardinals up to interpretability using arguably
informal cosmological ideas. We regard this as part of Concept Calculus.
1. OEU = Outer Exploding Universe.
2. Alternative Axiomatization of OEU.
3. IEU = Inner Exploding Universe.
4. The System IEU#.
1. OEU = OUTER EXPLODING UNIVERSE.
The language of OEU is L = predicate calculus with equality and the
following nonlogical symbols
i. Binary predicate symbol <.
ii. The unary predicate symbol D.
iii. Unary function symbol F.
In OEU, we think of two universes. There is the "present universe" in
the sense of all axiom systems in predicate calculus. And there is the
"initial universe" carved out by D. We think of D as the initial
universe which has exploded into the present universe.
We think of universes as having one dimensional space. In this initial
version, we will not exploit sophisticated spatial structure.
We think of < as a strict linear ordering on one dimensional space.
As in standard scientific physics, one dimensional space also serves
as the space of quantities. I.e., the one dimensional space of
nonnegative real numbers.
The function F assigns a quantity to every point in the present
universe.
We think of F as the "radiation function", where F(x) provides a
quantity of radiation at the point x.
The Explosion axiom asserts that there is a point in the present
universe that is not in the initial universe.
The Stability axiom asserts that if a given point in the initial
universe is related, in some specific way, to a point in the present
universe, then the given point is related, in the same specific way,
to a point in the initial universe.
The final axiom is the Plentitude axiom.
The Principle of Plentitude goes back to Aristotle, and can be
asserted in many contexts. See, e.g., http://en.wikipedia.org/wiki/Plenitude_principle
where Aristotle is quoted as saying
*no possibilities which remain eternally possible will go unrealized*
In our context, we can take this to assert that
*any pattern of radiation is realized in some interval [x,y]*
There are some interesting issues involved in formally treating
"patterns of radiation". Obviously, one crude aspect of "patterns of
radiation" is the set of magnitudes of the radiation. I.e., the set of
values of F.
So we are led to consider the principle
*any given set of points is the set of values of F on some interval
[x,y]*
However, the above leads to a Russell Paradox style inconsistency. The
appropriate formulation of this principle is
*any given upper bounded set of points is the set of values of F on
some interval [x,y]*
The above, when formulated as a scheme for the initial universe, is
called Plentitude.
We are now prepared to give the formal axioms.
THE SYSTEM OEU.
For readability, we write x in D for D(x).
LINEARITY. < is a strict linear ordering.
EXPLOSION. (therexists x)(x not in D).
STABILITY. Let x in D. There exists y such that A(s,y) if and only if
there exists y in D such that A(x,y). Here A is a formula of L with at
most the free variables x,y, in which D does not appear.
PLENTITUDE. Any subset of D, bounded (<=) above by some element of D,
and definable by a formula of L (parameters allowed), is the set of
values of F at the elements of some open interval (x,y), x,y in D.
THEOREM 1.1. OEU and ZF are mutually interpretable. This is provable
in EFA.
2. ALTERNATIVE AXIOMATIZATION OF OEU.
Let OEU' be
LINEARITY. < is a strict linear ordering.
OUTER EXPLOSION. (therexists x)(x not in D). (forall x < y)(y in D
implies x in D).
STABILITY. Let x in D. There exists y such that A(s,y) if and only if
there exists y in D such that A(x,y). Here A is a formula of L with at
most the free variables x,y, in which D does not appear.
D-PLENTITUDE. Any subset of D, bounded (<=) above by some element of
D, and definable by a formula of L (parameters allowed), is the set of
values of F at the elements in D of some open interval (x,y), x,y in D.
THEOREM 2.1. OEU and OEU' are logically equivalent.
3. IEU = INNER EXPLODING UNIVERSE.
Instead of the Outer Explosion axiom, we use the Inner Explosion
axiom, which asserts that there is a least initial point which is
greater than some non initial point.
We add a Core Stability axiom that replaces "x in D" with (forall y <=
x)(y in D).
THE SYSTEM IEU.
LINEARITY. < is a strict linear ordering.
INNER EXPLOSION. There exists a least x in D greater than some y not
in D.
STABILITY. Let x in D. There exists y such that A(s,y) if and only if
there exists y in D such that A(x,y). Here A is a formula of L with at
most the free variables x,y, in which D does not appear.
D-PLENTITUDE. Any subset of D, bounded (<=) above by some element of
D, and definable by a formula of L (parameters allowed), is the set of
values of F at the elements in D of some open interval (x,y), x,y in D.
CORE STABILITY. Let (forall z <= x)(z in D). There exists y such that
A(x,y) if and only if there exists y such that (forall z <= y)(z in D)
and A(x,y). Here A is a formula of L with at most the free variables
x,y, in which D does not appear.
Let T be ZF + "there exists a nontrivial elementary embedding from
some V(alpha) into some V(beta) with critical point kappa such that
V(kappa) is a proper elementary substructure of V(alpha)" stated as a
scheme on the complexity of formulas.
THEOREM 3.1. IEU and T are mutually interpretable.
Old fashioned technology shows that T proves the consistency of ZFC +
"there are arbitrarily large measurable cardinals" and more. From oral
communications, core model technology shows that T proves the
consistency of ZFC + "there exist arbitrarily large Woodin cardinals"
and more. Woodin thinks that T probably proves the consistency of ZFC
+ "there exists a supercompact cardinal".
4. THE SYSTEM IEU#
IEU# is IEU together with the axiom
INACCESSIBILITY. (forall x < a)(therexists y in D)(A) implies
(therexists z in D)(forall x < a)(therexists y < z)(y in D and A).
Here A is a formula of L in which z is not free.
THEOREM 4.1. IEU# is equiconsistent with NBG + j:V into V + V(kappa)
is an elementary substructure of V.
Woodin has shown that the theory in Theorem 4.1 proves the consistency
of ZFC + I0 and more. Hence the consistency of IEU# implies the
consistency of ZFC + IO and more.
**********************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 444th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-349 can be found athttp://www.cs.nyu.edu/pipermail/fom/2009-August/014004.html
in the FOM archives.
350: one dimensional set series 7/23/09 12:11AM
351: Mapping Theorems/Mahlo/Subtle 8/6/09 10:59PM
352: Mapping Theorems/simpler 8/7/09 10:06PM
353: Function Generation 1 8/9/09 12:09PM
354: Mahlo Cardinals in HIGH SCHOOL 1 8/9/09 6:37PM
355: Mahlo Cardinals in HIGH SCHOOL 2 8/10/09 6:18PM
356: Simplified HIGH SCHOOL and Mapping Theorem 8/14/09 9:31AM
357: HIGH SCHOOL Games/Update 8/20/09 10:42AM
358: clearer statements of HIGH SCHOOL Games 8/23/09 2:42AM
359: finite two person HIGH SCHOOL games 8/24/09 1:28PM
360: Finite Linear/Limited Memory Games 8/31/09 5:43PM
361: Finite Promise Games 9/2/09 7:04AM
362: Simplest Order Invariant Game 9/7/09 11:08AM
363: Greedy Function Games/Largest Cardinals 1
364: Anticipation Function Games/Largest Cardinals/Simplified 9/7/09
11:18AM
365: Free Reductions and Large Cardinals 1 9/24/09 1:06PM
366: Free Reductions and Large Cardinals/polished 9/28/09 2:19PM
367: Upper Shift Fixed Points and Large Cardinals 10/4/09 2:44PM
368: Upper Shift Fixed Point and Large Cardinals/correction 10/6/09
8:15PM
369. Fixed Points and Large Cardinals/restatement 10/29/09 2:23PM
370: Upper Shift Fixed Points, Sequences, Games, and Large Cardinals
11/19/09 12:14PM
371: Vector Reduction and Large Cardinals 11/21/09 1:34AM
372: Maximal Lower Chains, Vector Reduction, and Large Cardinals
11/26/09 5:05AM
373: Upper Shifts, Greedy Chains, Vector Reduction, and Large
Cardinals 12/7/09 9:17AM
374: Upper Shift Greedy Chain Games 12/12/09 5:56AM
375: Upper Shift Clique Games and Large Cardinals 1graham
376: The Upper Shift Greedy Clique Theorem, and Large Cardinals
12/24/09 2:23PM
377: The Polynomial Shift Theorem 12/25/09 2:39PM
378: Upper Shift Clique Sequences and Large Cardinals 12/25/09 2:41PM
379: Greedy Sets and Huge Cardinals 1
380: More Polynomial Shift Theorems 12/28/09 7:06AM
381: Trigonometric Shift Theorem 12/29/09 11:25AM
382: Upper Shift Greedy Cliques and Large Cardinals 12/30/09 2:51AM
383: Upper Shift Greedy Clique Sequences and Large Cardinals 1
12/30/09 3:25PM
384: THe Polynomial Shift Translation Theorem/CORRECTION 12/31/09
7:51PM
385: Shifts and Extreme Greedy Clique Sequences 1/1/10 7:35PM
386: Terrifically and Extremely Long Finite Sequences 1/1/10 7:35PM
387: Better Polynomial Shift Translation/typos 1/6/10 10:41PM
388: Goedel's Second Again/definitive? 1/7/10 11:06AM
389: Finite Games, Vector Reduction, and Large Cardinals 1 2/9/10
3:32PM
390: Finite Games, Vector Reduction, and Large Cardinals 2 2/14/09
10:27PM
391: Finite Games, Vector Reduction, and Large Cardinals 3 2/21/10
5:54AM
392: Finite Games, Vector Reduction, and Large Cardinals 4 2/22/10
9:15AM
393: Finite Games, Vector Reduction, and Large Cardinals 5 2/22/10
3:50AM
394: Free Reduction Theory 1 3/2/10 7:30PM
395: Free Reduction Theory 2 3/7/10 5:41PM
396: Free Reduction Theory 3 3/7/10 11:30PM
397: Free Reduction Theory 4 3/8/10 9:05AM
398: New Free Reduction Theory 1 3/10/10 5:26AM
399: New Free Reduction Theory 2 3/12/10 9:36AM
400: New Free Reduction Theory 3 3/14/10 11:55AM
401: New Free Reduction Theory 4 3/15/10 4:12PM
402: New Free Reduction Theory 5 3/19/10 12:59PM
403: Set Equation Tower Theory 1 3/22/10 2:45PM
404: Set Equation Tower Theory 2 3/24/10 11:18PM
405: Some Countable Model Theory 1 3/24/10 11:20PM
406: Set Equation Tower Theory 3 3/25/10 6:24PM
407: Kernel Tower Theory 1 3/31/10 12:02PM
408: Kernel tower Theory 2 4/1/10 6:46PM
409: Kernel Tower Theory 3 4/5/10 4:04PM
410: Kernel Function Theory 1 4/8/10 7:39PM
411: Free Generation Theory 1 4/13/10 2:55PM
412: Local Basis Construction Theory 1 4/17/10 11:23PM
413: Local Basis Construction Theory 2 4/20/10 1:51PM
414: Integer Decomposition Theory 4/23/10 12:45PM
415: Integer Decomposition Theory 2 4/24/10 3:49PM
416: Integer Decomposition Theory 3 4/26/10 7:04PM
417: Integer Decomposition Theory 4 4/28/10 6:25PM
418: Integer Decomposition Theory 5 4/29/10 4:08PM
419: Integer Decomposition Theory 6 5/4/10 10:39PM
420: Reduction Function Theory 1 5/17/10 2:53AM
421: Reduction Function Theory 2 5/19/10 12:00PM
422: Well Behaved Reduction Functions 1 5/23/10 4:12PM
423: Well Behaved Reduction Functions 2 5/27/10 3:01PM
424: Well Behaved Reduction Functions 3 5/29/10 8:06PM
425: Well Behaved Reduction Functions 4 5/31/10 5:05PM
426: Well Behaved Reduction Functions 5 6/2/10 12:43PM
427: Finite Games and Incompleteness 1 6/10/10 4:08PM
428: Typo Correction in #427 6/11/10 12:11AM
429: Finite Games and Incompleteness 2 6/16/10 7:26PM
430: Finite Games and Incompleteness 3 6/18/10 6:14PM
431: Finite Incompleteness/Combinatorially Simplest 6/20/10 11:22PM
432: Finite Games and Incompleteness 4 6/26/10 8:39PM
433: Finite Games and Incompleteness 5 6/27/10 3:33PM
434: Digraph Kernel Structure Theory 1 7/4/10 3:17PM
435: Kernel Structure Theory 1 7/5/10 5:55PM
436: Kernel Structure Theory 2 7/9/10 5:21PM
437: Twin Prime Polynomial 7/15/10 2:01PM
438: Twin Prime Polynomial/error 9/17/10 1:22PM
439: Twin Prime Polynomial/corrected 9/19/10 2:16PM
440: Finite Phase Transitions 9/26/10 1:28PM
441: Equational Representations 9/27/10 4:59PM
442: Kernel Structure Theory Restated 10/11/10 9:01PM
443: Kernels and Large Cardinals 1 10/21/10 12:16AM
Harvey Friedman
More information about the FOM
mailing list