[FOM] 511: A Supernatural Consistency Proof for Mathematics
Harvey Friedman
hmflogic at gmail.com
Thu Jan 10 21:19:13 EST 2013
THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION
*****************************************
THIS POSTING IS ENTIRELY SELF CONTAINED
*****************************************
In http://www.math.osu.edu/~friedman.8/manuscripts.html #75 we gave A
Divine Consistency Proof for Mathematics.
That Divine system has objects and classes of objects, and relies on
the notion of "positive class of objects", a notion going back to
Goedel, Liebniz, and others, connected with Theology. The purely
mathematical infrastructure in the Divine system consists of standard
comprehension, ordered pairing on objects, extensionality, and a
choice operator (formulated with a unary function symbol). This alone
is not enough to prove the consistency of ZFC, but rather corresponds
to Z_2. Additional axioms are added involving positivity to achieve
very high strength.
This Divine approach does not accommodate God as an object, for then
"positive classes of objects" becomes trivial.
So we became interested in seeing how the consistency of mathematics
can be proven using rudimentary theological ideas, with God allowed as
an object, and without using positivity.
We have been successful with this, providing a Supernatural
Consistency Proof as an alternative to the Divine Consistency Proof.
{REMARK: What seems to be emerging is the prospect of a growing number
of consistency proofs for mathematics that are based on various basic
extra mathematical conceptions. As noted in the Divine Consistency
paper, what is done there, and also what is done here, is part of a
much more general program called Concept Calculus.
CONJECTURE. In ANY informal conceptual environment, we can formulate
principles that are natural and sensitive and plausible in that
environment, which are mutually interpretable with ZFC, and weak and
strong variants of ZFC.}
It turns out that we can incorporate God, but only if we incorporate
lots of supernatural objects in addition to God.
The purely mathematical infrastructure in this new Supernatural system
is identical to the Divine system: standard comprehension, ordered
pairing on objects, extensionality, and a choice operator (formulated
with a unary function symbol).
We add a constant symbol RO for the class of all real objects,
together with the obvious axiom: THERE IS AN OBJECT NOT IN RO.
Here is the fundamental principle we use.
SUPERNATURAL REDUCTION. ANY PROPERTY NOT MENTIONING RO THAT HOLDS OF A
GIVEN REAL OBJECT, ALSO HOLDS OF THE OBJECT IF THE QUANTIFIERS ARE
RESTRICTED TO RO. AND SUBCLASSES OF RO.
So this system avoids use of Positivitu - a crucial feature in the
Divine system - at the cost of introducing RO (or alternatively,
expanding with supernatural objects). The logical strength under this
new approach is considerably weaker, yet it is still much stronger
than ZFC.
THE FORMAL PRESENTATION
We have two sorts: objects and classes (of objects). We use variables
v_i over objects and variables A_i over classes. We use = between
objects, and = between classes, epsilon (membership) between objects
and classes, and the class constant symbol RO (class of real objects).
We use the binary function symbol P from and into objects (ordered
pairing). We use F for a unary function symbol from classes to objects
(choice operator).
The nonlogical axioms are as follows. For readability, we use "in" for
membership.
COMPREHENSION.
(therexists A)(forall v)(v in A iff phi), where phi is any formula in
the language in which A is not free.
PAIRING.
P(x,y) = P(z,w) implies x = z and y = w.
CHOICE.
v in A implies F(A) in A.
EXTENSIONALITY.
(forall v)(v in A iff v in B) implies A = B.
SUPERNATURAL REDUCTION.
v in RO and phi implies phi*, where phi is a formula in the language
without RO, with at most the free variable v, and phi* results from
relativizing the object quantifiers in phi to RO and the class
quantifiers in RO to subclasses of RO.
SUPERNATURAL EXISTENCE.
(therexists v)(v not in RO).
THEOREM. This system is mutually interpretable with ZFC + {there
exists a Sigma-2-n indescribable cardinal}_n. In particular, ZFC is
interpretable in the system, and the consistency of the system
provably implies the consistency of ZFC, within EFA = exponential
function arithmetic.
An alternative formulation is to disallow = between classes, drop
Extensionality, and strengthen Choice, adding that if A,B have the
same elements, then F(A) = F(B). Also simplify Supernatural Reduction
to
SUPERNATURAL REDUCTION (simplified).
v in RO and phi implies phi*, where phi is a formula in the language
without RO, with at most the free variable v, and phi* results from
relativizing the object quantifiers in phi to RO.
The same Theorem holds for this modified system.
*****************************************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 511th 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
Harvey Friedman
More information about the FOM
mailing list