[FOM] 554: Foundational Methodology 5/Maximality

[Harvey Friedman]

Continuation from http://www.cs.nyu.edu/pipermail/fom/2014-October/018239.html

Here we discuss some kinds of "logical maximality".

Let T be a theory in the first order predicate calculus with equality,
with finitely many constant, relation, and function symbols. We assume
that T is given by individual axioms and  axiom schemes. A
particularly important case is where there are finitely many axioms
and finitely many axiom schemes.

We define the associated theory T(extend), whose language is that of T
extended with a new unary predicate symbol P. The axioms of T(extend)
are

1. The extension of P contains the constants and is closed under the functions.
2. The axioms, and the schemes of T, the latter being treated as
schemes in the extended language.
3. The axioms of T, with quantifiers relativized to P.
4. The schemes of T, with quantifiers relativized to P.  These schemes
are treated as schemes in the extended language.

Note that the models of T(extend) are the (M,P), where M is a model of
T and P carves out a submodel of T, where in both cases the schemes
are taken over all formulas in the extended language.

We say that T is logically maximal if and only if T(extend) proves
(forall x)(P(x)). I.e., every such (M,P) above has P = dom(M).

THEOREM 1. PA (Peano arithmetic) is logically maximal. Z_2 (formulated
as a single sorted theory in the obvious way) is logically maximal.
More generally, for n >= 2, Z_n (formulated as a single sorted theory
in the obvious way) is logically maximal. However, no consistent
extension of Z by axioms is logically maximal.

The last negative claim is rather cheap. Consideration of it suggests
a stronger notion.

Let T be as above. We define the associated theory T(elex), for
elementary extension. Of course it is stronger than elementary
extension. T(elex) has language that of T extended with a new unary
predicate symbol P as before. The axioms of T(elex) are

1. The extension of P carves out an elementary substructure with
respect to the language of T.
2. The axioms, and the schemes of T, the latter being treated as
schemes in the extended language.
3. The axioms of T, with quantifiers relativized to P.
4. The schemes of T, with quantifiers relativized to P. These schemes
are treated as schemes in the extended language.

Note that the models of T(elex) are the (M,P), where M is a model of T
and P carves out an elementary submodel of M for the language of T,
where for both M and the submodel, the schemes hold when taken over
formulas in the extended language.

We say that T is elementarily maximal if and only if T(elex) proves
(forall x)(P(x)). I.e., every such (M,P) above has P = dom(M).

Note that elementarily maximal is a nice logical notion. Let's see
what happens when we apply it to ZFC and its extensions.

THEOREM 2. Logically maximal implies elementarily maximal (trivial).
ZC + "every set has rank some omega + n" is elementarily maximal. No
consistent extension of ZF by axioms is elementarily maximal.

Another example is the real closed fields. There are two particularly
well known axiomatizations. One is ordered field, every positive
element has a square root, every moonic polynomial of odd degree has a
root. The second is ordered field, plus the scheme of least upper
bound.

THEOREM 3. The first axiomatization of real closed fields is not
elementarily maximal. The second axiomatization of real closed fields
is logically maximal.

Next time I want to get into real set theoretic issues. Particularly,
the relationship between "intrinsic maximality of the set theoretic
universe" and the existence(?) of a nonconstructible subset of omega.

************************************************************
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 554th 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  10/21/14 9:59AM
553: Foundational Methodology 4/Maximality  10/21/14 11:57AM

Harvey Friedman