[FOM] 513: Five Supernatural Consistency Proofs for Mathematics

Harvey Friedman hmflogic at gmail.com
Mon Jan 14 01:13:19 EST 2013



but follows up on


There has been some major developments in the Consistency Proofs.

I now put all of these Consistency Proofs, based on rudimentary ideas
from philosophical theology, under the umbrella


This means that we are proving the consistency of mathematics, and
various extensions of mathematics with strong set theoretic
principles, using simple fundamental principles about the
Supernatural. The key axioms reflect relationships between the Real
World and the wider Supernatural World. The axioms assert

i. The Supernatural World is more extensive, in certain respects, than
the Real World.
ii. The Real World and the Supernatural World are similar in other respects.

In the case of the Divine Consistency Proof, the principles are very
close to those that have been extensively discussed in the context of
Theology, with Ontological Arguments, following Goedel, Leibniz, and
others. Furthermore, there is no Supernatural World reflected directly
in the formalism. The key concept of Positive Property is viewed as
something of Supernatural origin - i.e., from God. But it is applied
to the Real World only.

In contrast, the new ones, including the one from posting #511,
directly incorporate the Supernatural World.

Each of this line of consistency proofs has its own subtitle. We now
have Five Consistency Proofs. To keep this posting self contained, we
will present the formal axioms for all five here.

1. Divine Consistency Proof. See
http://www.math.osu.edu/~friedman.8/manuscripts.html #75

It was shown in #75 that the Divine system corresponds to something a
little weaker than a measurable cardinal.

2. Equivalence Consistency Proof. This is the new name for the
"Supernatural Consistency Proof" of
http://www.cs.nyu.edu/pipermail/fom/2013-January/016881.html This
system has strength just under a second order indescribable cardinal.
This is much weaker than 1.

3. First Extension Consistency Proof. This is new, and avoids all use
of Choice. It replaces Choice with Supernatural Plenitude.The key
axiom asserts that we can extend any class in the real world to a
class in the wider (supernatural) world, where both have the same
properties from the point of view of the respective worlds in which
they reside. This has the same strength as 2, and therefore much
weaker than 1.

4. Second Extension Consistency Proof. This is new, and uses Choice,
but not Supernatural Plenitude. It uses the same key extending axiom.
We know that this is much stronger than 2,3. At least the strength of
0# and a lot more. This is much stronger than 2,3, and may be as
strong as 1.

5. Third Extension Consistency Proof. This is new, and combines 3 and
4. It uses the same key extending axiom, but has both Choice and
Supernatural Plenitude. This is weaker than a 1-extendible cardinal
and stronger than a superstrong cardinal. This is much stronger than
1,2,4, and at least what we are claiming about 3.

REMARKS ON CHOICE. We are agnostic about how important it is or isn't
to eliminate use of Choice. Therefore, by default, it becomes at least
valuable to eliminate use of Choice. There is some detailed motivation
of the axioms of the Divine System below, including Choice, in
http://www.math.osu.edu/~friedman.8/manuscripts.html #75. In essence,
a theologically reasonable position might be: God gave us these
facilities (including a Choice Operator), and we created mathematics,
or interpretations of mathematics, using them.


We now present four systems. Three of them are based on somewhat
different languages. There are many common axioms. In each case Full
Comprehension is always

(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 (which varies
some from system to system), in which A_1 is not free.


The language L(divine) is based on

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).
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).


P(v_1,v_2) = P(v_3,v_4) implies v_1 = v_3 and v_2 = v_4.


(for all v_1)(v_1 in A_1 iff v_1 in A_2) implies A_1 = A_2.


v_1 in A_1 implies CHO(A_1) in A_1.



(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).


(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,
with at most the free variables v_1,A_2,...,A_n, n >= 1.


(there exists v_1)(for all A_1)(DEF(A_1) and POS(A_1) implies v_1 in A_1).


The language L(equiv) is based on

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).
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), we let phi* be the result of
replacing quantifiers (Qv), (QA) in phi by (Qv in RO), (QA contained
in RO). We can expand phi* into primitive notation in the usual way.
This same definition is also made for formulas phi in L(extend_1),
L(extend_2), L(extend_3).



(there exists v_1)(v_1 not in RO).


v_1 in RO implies (phi iff phi*), where phi is a formula of L(equiv)
without RO, whose free variables are among v_1.


The language L(extend_1) is based on L(equiv)  without CHO, plus a
unary function symbol F from objects to classes (supernatural
plenitude function).



A_1 contained in RO implies (there exists v_1)(F(v_1) = A_1).


phi* 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
with free variable at most A_1, A_2 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.


The language L(extend_2) is the same as the language L(equiv).



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


Note that Supernatural Existence follows from Supernatural Plenitude.

THEOREM 1. All five systems interpret ZFC. All five systems are
interpretable in ZFC + "there exists a 1-extendible cardinal".

THEOREM 2. Divine System is interpretable in ZFC + "there exists a
measurable cardinal" and is interpretable in ZFC + "there are
arbitrarily large strong Ramsey cardinals". Equivalence System and
First Extension System are each mutually interpretable with ZFC +
{there is a Sigma-2-n indescribable cardinal}_n. Second Extension
System is interpretable is interpretable in ZFC + "there is a
1-extendible cardinal" and interprets ZFC + "for all x contained in
omega, x# exists". Third Extension System is interpretable in ZFC +
"there is a 1-extendible cardinal" and interprets ZFC + "there is a
superstrong cardinal".


I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 513th 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

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

Harvey Friedman

More information about the FOM mailing list