[FOM] 515: Eight Supernatural Consistency Proofs For Mathematics
Harvey Friedman
hmflogic at gmail.com
Sat Jan 19 14:40:49 EST 2013
THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION
*****************************************
THIS POSTING IS ENTIRELY SELF CONTAINED
but follows up on http://www.cs.nyu.edu/pipermail/fom/2013-January/016887.html
*****************************************
We add to our inventory of 5 Consistency Proofs from posting #513,
http://www.cs.nyu.edu/pipermail/fom/2013-January/016887.html.
We also correct the claims about the strengths of the second and third
Extension Systems - they are weaker than indicated in
http://www.cs.nyu.edu/pipermail/fom/2013-January/016887.html.
We restate all of them. We now have both the First Equivalence System and
the Second Equivalence System, and two more Extension systems.
We also make some improvements in the notation and presentation.
We refer to all of them as Supernatural Consistency Proofs. Obviously
some of the systems extend others. If we just want to prove the
consistency of mathematics as formalized by ZFC, then the best is
probably the First Equivalence System, and if in addition, we want to
avoid use of the Supernatural World, and just use a shadow of it on
the Real World, then of course the Divine System is the only one of
the 7 that meets that criteria (the one that uses positive classes (of
real objects only)). The First Extension System might be focused on,
because of its avoidance of choice altogether.
But the stronger systems also prove the consistency of the stronger
form of mathematics that is augmented by large cardinal hypotheses of
various strengths. As we have noted, the Divine System also
accomplishes this purpose.
These 8 Consistency Proofs show that, in various ways, we can very
naturally interpret set theory in *flat* systems. I.e., in a very
natural way, we do not have to rely on anything like the cumulative
hierarchy, or iterative notion of set. Objects and classes of objects
suffice, and in this very limited two sorted context, membership is
vividly understandable and universally familiar.
Recall these two general principles, as discussed in
http://www.cs.nyu.edu/pipermail/fom/2013-January/016887.html
i. The Supernatural World is more extensive than the Real World.
ii. The Real World and the Supernatural World are similar in various respects.
1. DIVINE SYSTEM.
2. FIRST EQUIVALENCE SYSTEM.
3. SECOND EQUIVALENCE SYSTEM.
4. FIRST EXTENSION SYSTEM.
5. SECOND EXTENSION SYSTEM.
6. THIRD EXTENSION SYSTEM.
7. STRONG EXTENSION SYSTEM.
8. EXTREME EXTENSION SYSTEM.
We now present these seven systems.
NOTE: Obviously systems 2-7 have the flavor of very strong forms of
nonstandard analysis. With system 1, the connection is much less
clear. Goedel wrote a couple of paragraphs about Nonstandard Analysis.
See
K. Goedel, Remark on non-standard analysis, 1974, in: Goedel's
Collected Works, volume 2, p. 307 -310 (J.E. Fenstad) and p. 311 (K.
Goedel) .
The language of these systems vary, but they all contain at least the
following components:
i. variables v_i over objects .
ii. variables A_i over classes (of objects).
iii. = between objects.
iv. = between classes.
v. binary function symbol P on objects (ordered pairing).
vi. binary relation symbol epsilon between objects and classes (membership).
In every one of the systems, we use the following.
LOGIC (usual axioms and rules of logic for the language of the system)
PAIRING
P(v_1,v_2) = P(v_3,v_4) implies v_1 = v_3 and v_2 = v_4.
EXTENSIONALITY
(for all v_1)(v_1 in A_1 iff v_1 in A_2) implies A_1 = A_2.
FULL COMPREHENSION
(there exists A_1)(for all v_1)(v_1 in A_1 iff phi)
where phi is a formula of the language of the system in which A_1 is not free.
*DIVINE SYSTEM*
the original one based on Goedel's positive properties
The language L(divine) is based on
i - vi.
vii. unary function symbol CH from classes to objects (choice operator).
viii. unary predicate symbol POS on classes (positive class, going
back to Goedel and Leibniz, etc.).
ix. unary predicate DEF on classes (class is definable using i-viii
without parameters).
LOGIC, PAIRING, EXTENSIONALITY, FULL COMPREHENSION, CHOICE OPERATOR,
POSITIVE CLASSES, 0-DEFINABLE CLASSES, DIVINE OBJECT..
CHOICE OPERATOR
v_1 in A_1 implies CHO(A_1) in A_1.
POSITIVE CLASSES
(for all v_1)(v_1 in A_1 or v_1 in A_2) implies POS(A_1) or POS(A_2).
POS(A_1) and POS(A_2) implies (there exists v_1 not= v_2)(v_1,v_2 in
A_1 and v_1,v_2 in A_2).
0-DEFINABLE CLASSES
(for all v_1)(v_1 in A_1 iff phi) ∧ DEF(A_2) and ... and DEF(A_n)
implies DEF(A_1)
where phi is a formula of L(divine) without DEF, whose ee variables
are among v_1,A_2,...,A_n, n >= 1.
DIVINE OBJECT
(there exists v_1)(for all A_1)(DEF(A_1) and POS(A_1) implies v_1 in A_1).
*FIRST EQUIVALENCE SYSTEM*
The language L(equiv_1) is based on
i - vi.
vii. unary function symbol CH from classes to objects (choice operator).
viii. class constant symbol RO (class of all real objects).
For any formula phi in L(equiv_1), we let phi/RO be the result of
replacing quantifiers (Qv), (QA) in phi by (Qv in RO), (QA contained
in RO). We can expand phi/RO into primitive notation in the usual way.
LOGIC, PAIRING, EXTENSIONALITY, FULL COMPREHENSION, CHOICE OPERATOR,
SUPERNATURAL EXISTENCE, REAL/SUPERNATURAL EQUIVALENCE.
SUPERNATURAL EXISTENCE
(there exists v_1)(v_1 not in RO).
REAL/SUPERNATURAL EQUIVALENCE
v_1 in RO implies (phi iff phi*)
where phi is a formula of L(equiv_1) without RO, where every free
variable is v_1.
*SECOND EQUIVALENCE SYSTEM*
The language L(equiv_2) is L(equiv_1) together with the unary
function symbol C from objects to objects.
LOGIC, PAIRING, EXTENSIONALITY, FULL COMPREHENSION, CHOICE OPERATOR,
SUPERNATURAL EXISTENCE, REAL/SUPERNATURAL EQUIVALENCE,
CORRESPONDENCE..
CORRESPONDENCE
(for all v_1,v_2)(C(v_1) in RO and (C(v_1) = C(v_2) implies v_1 = v_2)).
*FIRST EXTENSION SYSTEM*
The language L(extend_1) is based on L(equiv_1) without CHO, and plus a
unary function symbol F from objects to classes (supernatural
plenitude function).
LOGIC, PAIRING, EXTENSIONALITY, FULL COMPREHENSION, SUPERNATURAL
PLENITUDE, SUPERNATURAL PLENITUDE, SUPERNATURAL EXTENSION.
SUPERNATURAL PLENITUDE
A_1 contained in RO implies (there exists v_1)(F(v_1) = A_1).
Note that Supernatural Existence follows from Supernatural Plenitude.
SUPERNATURAL EXTENSION
phi/RO and A_1 contained in RO implies (there exists A_2)(A_1 = A_2
intersect RO and phi[A_1/A_2])
where phi is a formula in =,epsilon,P
where all free variables are A_1, and A_2 is not bound in phi, and phi[A_1/A_2]
is the result of replacing all free occurrences of A_1 in phi by A_2.
*SECOND EXTENSION SYSTEM*
The language L(extend_2) is the same as the language L(equiv_1).
LOGIC, PAIRING, EXTENSIONALITY, CHOICE OPERATOR, FULL COMPREHENSION,
SUPERNATURAL EXISTENCE, SUPERNATURAL EXTENSION.
*THIRD EXTENSION SYSTEM*
The language L(extend_3) is the based on L(extend_1) plus L(extend_2).
The axioms are those of the First and Second Extension Systems, which
comprise
LOGIC, PAIRING, EXTENSIONALITY, FULL COMPREHENSION, CHOICE OPERATOR,
SUPERNATURAL PLENITUDE, SUPERNATURAL EXTENSION..
*STRONG EXTENSION SYSTEM*
THe language L(s-extend) is the same as the language L(equiv_1).
LOGIC, PAIRING, EXTENSIONALITY, CHOICE OPERATOR, FULL COMPREHENSION,
SUPERNATURAL EXISTENCE, SUPERNATURAL EXTENSION, CORRESPONDENCE.
*EXTREME EXTENSION SYSTEM*
L(extreme) is L(equiv_1) plus
a unary function symbol * from classes to classes (extension operator)
a unary function symbol H from objects to classes.
LOGIC, PAIRING, EXTENSIONALITY, FULL COMPREHENSION, CHOICE OPERATOR,
GLOBAL EXTENSION, BIJECTION.
GLOBAL EXTENSION
v_1,...,v_n in RO and A_1,...,Am contained in RO implies (phi/RO iff
phi[A1/A1*,...,A_m/A_m*])
where all free variables of phi are among v_1,...,v_n,A_1,...,A_m, n,m >= 0.
BIJECTION
H is a bijection from the objects onto the A contained in RO such that A* = A.
NOTE: Under this formalization, the * operator is relevant only applied to
subclasses of RO.
NOTE: An alternative axiomatization that is equivalent, and perhaps
closer to intuition, is to have a symbol for a one-one map from
objects, to objects in RO, and also a symbol for a one-one map from
the A contained in RO with A* = A, into objects.
THEOREM 1. All seven systems interpret ZFC. All seven systems are
interpretable in ZFC + "there exists a nontrivial elementary embedding
from some V(lambda+1) into V(lambda+1)".
THEOREM 2. The Divine System is interpretable in ZFC + "there exists a
measurable cardinal" and interprets ZFC + "there are
arbitrarily large strong Ramsey cardinals".
THEOREM 3. The First Equivalence System and the
First, Second, Third Extension Systems are each mutually interpretable
with ZFC +
{there is a Sigma-2-n indescribable cardinal}_n.
THEOREM 4. The Second Equivalence System and the Strong Extension
System each interpret ZFC + "for all x contained in
omega, x# exists".
THEOREM 5. The Extreme Extension System interprets ZFC + "there exists
a nontrivial elementary embedding from some V(lambda) into V(lambda),
and even I2 (and somewhat more).
THEOREM 6. All of these interpretations are carried out provably in
EFA = exponential function arithmetic, and therefore support
corresponding relative consistency proofs, within EFA.
*****************************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 515th 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-449 can be found
in the FOM archives at
http://www.cs.nyu.edu/pipermail/fom/2010-December/015186.html
450: Maximal Sets and Large Cardinals II 12/6/10 12:48PM
451: Rational Graphs and Large Cardinals I 12/18/10 10:56PM
452: Rational Graphs and Large Cardinals II 1/9/11 1:36AM
453: Rational Graphs and Large Cardinals III 1/20/11 2:33AM
454: Three Milestones in Incompleteness 2/7/11 12:05AM
455: The Quantifier "most" 2/22/11 4:47PM
456: The Quantifiers "majority/minority" 2/23/11 9:51AM
457: Maximal Cliques and Large Cardinals 5/3/11 3:40AM
458: Sequential Constructions for Large Cardinals 5/5/11 10:37AM
459: Greedy CLique Constructions in the Integers 5/8/11 1:18PM
460: Greedy Clique Constructions Simplified 5/8/11 7:39PM
461: Reflections on Vienna Meeting 5/12/11 10:41AM
462: Improvements/Pi01 Independence 5/14/11 11:53AM
463: Pi01 independence/comprehensive 5/21/11 11:31PM
464: Order Invariant Split Theorem 5/30/11 11:43AM
465: Patterns in Order Invariant Graphs 6/4/11 5:51PM
466: RETURN TO 463/Dominators 6/13/11 12:15AM
467: Comment on Minimal Dominators 6/14/11 11:58AM
468: Maximal Cliques/Incompleteness 7/26/11 4:11PM
469: Invariant Maximality/Incompleteness 11/13/11 11:47AM
470: Invariant Maximal Square Theorem 11/17/11 6:58PM
471: Shift Invariant Maximal Squares/Incompleteness 11/23/11 11:37PM
472. Shift Invariant Maximal Squares/Incompleteness 11/29/11 9:15PM
473: Invariant Maximal Powers/Incompleteness 1 12/7/11 5:13AMs
474: Invariant Maximal Squares 01/12/12 9:46AM
475: Invariant Functions and Incompleteness 1/16/12 5:57PM
476: Maximality, CHoice, and Incompleteness 1/23/12 11:52AM
477: TYPO 1/23/12 4:36PM
478: Maximality, Choice, and Incompleteness 2/2/12 5:45AM
479: Explicitly Pi01 Incompleteness 2/12/12 9:16AM
480: Order Equivalence and Incompleteness
481: Complementation and Incompleteness 2/15/12 8:40AM
482: Maximality, Choice, and Incompleteness 2 2/19/12 7:43AM
483: Invariance in Q[0,n]^k 2/19/12 7:34AM
484: Finite Choice and Incompleteness 2/20/12 6:37AM__
485: Large Large Cardinals 2/26/12 5:55AM
486: Naturalness Issues 3/14/12 2:07PM
487: Invariant Maximality/Naturalness 3/21/12 1:43AM
488: Invariant Maximality Program 3/24/12 12:28AM
489: Invariant Maximality Programs 3/24/12 2:31PM
490: Invariant Maximality Program 2 3/24/12 3:19PM
491: Formal Simplicity 3/25/12 11:50PM
492: Invariant Maximality/conjectures 3/31/12 7:31PM
493: Invariant Maximality/conjectures 2 3/31/12 7:32PM
494: Inv Max Templates/Z+up, upper Z+ equiv 4/5/12 4:17PM
495: Invariant Finite Choice 4/5/12 4:18PM
496: Invariant Finite Choice/restatement 4/8/12 2:18AM
497: Invariant Maximality Restated 5/2/12 2:49AM
498: Embedded Maximal Cliques 1 9/18/12 12:43AM
499. Embedded Maximal Cliques 2 9/19/12 2:50AM
500: Embedded Maximal Cliques 3 9/20/12 10:15PM
501: Embedded Maximal Cliques 4 9/23/12 2:16AM
502: Embedded Maximal Cliques 5 9/26/12 1:21AM
503: Proper Classes of Graphs 10/13/12 12:17PM
504. Embedded Maximal Cliques 6 10/14/12 12:49PM
505: Function Transfer Theory 10/21/12 2:15AM
506: Finite Embedded Weakly Maximal Cliques 10/23/12 12:53AM
507: Finite Embedded Dominators 11/6/12 6:40AM
508: Unique Undefinable Elements 12/22/12 8:08PM
509: A Divine Consistency Proof for Mathematics 12/26/12 2:15AM
510: Unique Undefinable Elements Again 1/9/13 5:07PM
511: A Supernatural Consistency Proof for Mathematics 1/10/13 9:19PM
512: Countable Elementary Extensions 1/11/13 7:31PM
513: Five Supernatural Consistency Proofs for Mathematics 1/14/13 1:13AM
514: Countable Elementary Extensions/again 1/14/13 2:19AM
Harvey Friedman
More information about the FOM
mailing list