[FOM] 553: Foundational Methodology 4/Maximality

[Harvey Friedman]

We have discussed elemental ways to express the Axiom of Choice in a
logical framework in #552.

THEOREM 1. AxC, over ZF, can be expressed in the form *such and such
(purely universal) sentence of predicate calculus with equality has a
model on any given infinite domain*, and also in the form *such and
such (purely universal) sentence of predicate calculus with equality
has a model on any given nonempty domain*

NOTE: I brought in the true Pi01 sentences into the previous
discussion, to formulate the priveleged position of AxC over ZF in
this logical realm. However, I should not have brought the Pi01
sentences in until I stated the above.

THEOREM 1. AxC cannot be expressed over ZF in the form *such and such
purely universal sentence of predicate calculus with equality in only
relation symbols has a model on any given infinite domain", nor in the
form *such and such purely universal sentence of predicate calculus
with equality in only relation symbols has a model on any given
nonempty domain". There is a decision procedure for the true ones of
these forms, and they all follow from ZF + "every set can be linearly
ordered".

We now want to discuss how we can express the Axiom of Choice as
"maximality", also in a logical framework.

QUESTION: Can AxC be expressed over ZF in the form *such and such a
purely universal sentence in relation symbols only, has a maximal
model on every nonempty domain*? Clearly, every such sentences are
provable in ZFC.

In the past, I would never throw out a possible jewel like the above
without putting a fair amount of effort into answering it. But I am 66
and trying to go into new fields like piano, math physics, mechanics,
statistics, etc., to make good on a teenage ambition. So if by good
fortune, the above Question turns out to be a jewel (maybe, maybe
not), have fun.

THEOREM 2. AxC, over ZF, can be expressed in the following form. Every
model of such and such purely universal sentence with relations only,
has a maximal extension with the same underlying domain, satisfying
the same purely universal sentence with relations only. Clearly, every
such sentence is provable in ZFC.

Proof: Use R,S,P, where R,S are binary and P is unary. Assert that

i. R(x,y) iff not S(x,y).
ii. P(x) and P(y) implies R(x,y).

QED

PROJECTS. We would like to get a general understanding of what
sentences over ZF can be expressed in these various ways. Various test
problems can be formulated, including decision procedure issues.

Consider countable choice, dependent choice, and "the reals are well
ordered". Can these be stated over ZF in any of the forms we have
discussed? Or if we restrict the forms above by restricting the
domains?

************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 553rd 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-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html

528: More Perfect Pi01  8/16/14  5:19AM
529: Yet more Perfect Pi01 8/18/14  5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01  8/22/14  5:16PM
532: More General Theory/Perfect Pi01  8/23/14  7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14  1:17AM
534: Perfect Explicitly Pi01  8/27/14  10:40AM
535: Updated Perfect Explicitly Pi01  8/30/14  2:39PM
536: Pi01 Progress  9/1/14 11:31AM
537: Pi01/Flat Pics/Testing  9/6/14  12:49AM
538: Progress Pi01 9/6/14  11:31PM
539: Absolute Perfect Naturalness 9/7/14  9:00PM
540: SRM/Comparability  9/8/14  12:03AM
541: Master Templates  9/9/14  12:41AM
542: Templates/LC shadow  9/10/14  12:44AM
543: New Explicitly Pi01  9/10/14  11:17PM
544: Initial Maximality/HUGE  9/12/14  8:07PM
545: Set Theoretic Consistency/SRM/SRP  9/14/14  10:06PM
546: New Pi01/solving CH  9/26/14  12:05AM
547: Conservative Growth - Triples  9/29/14  11:34PM
548: New Explicitly Pi01  10/4/14  8:45PM
549: Conservative Growth - beyond triples  10/6/14  1:31AM
550: Foundational Methodology 1/Maximality  10/17/14  5:43AM
551: Foundational Methodology 2/Maximality  10/19/14 3:06AM
552: Foundational Methodology 3/Maximality

Harvey Friedman