[FOM] 547: Conservative Growth - Triples

[Harvey Friedman]

*This research was partially supported by the John Templeton
Foundation grant ID #36297. The opinions expressed here are those of
the author and do not necessarily reflect the views of the John
Templeton Foundation.

I clarified an issue with #546 in
http://www.cs.nyu.edu/pipermail/fom/2014-September/018191.html   E.g.,
Con(ZFC) is now "better than" not Con(ZFC).

****************

CONSERVATIVE GROWTH is a phrase I recently coined to describe a
unified foundational view of something that has come up in my work on
incompleteness already starting in the 1980s. I recently wrote about
aspects of it in my unnumbered FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-September/018177.html Aspects
were previously discussed at my lecture at Princeton earlier this year
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
#63.

The basic idea is that we have an intellectual process whereby we
enlarge a universe of objects once or a few or many times. We
postulate that the relationships between objects remain stable under
each enlargement. The most familiar case of this is of course
elementary substructure.

It turns out that this idea leads to some very basic formalisms of
wide ranging interpretation power, ranging from fragments of Peano
arithmetic all the way through the upper regions of the large cardinal
hierarchy.

The idea readily applies to set theory, where each structure is
assumed to be some reasonable set theoretic universe - e.g., a model
of ZFC. However, the idea in no way depends on the universes of
objects being anything close to a universe of sets, or even having
anything to do with set theory at all. In fact, in section 3 below,
where we are thinking of set theory, we merely assume that each
universe satisfies only bounded separation, and each universe is an
element of the next universe. In other key applications, we will not
be thinking of set theoretic universes at all.

I applied, what is in retrospect, conservative growth of countable
sets of subsets of N, as a principal tool in my Borel incompleteness
theorems from the 1980's. I was only thinking of Borel incompleteness
at the time, and nowadays I do Pi01 incompleteness. In the old days, I
was doing Pi13 and Pi12 incompleteness, so that at least I was showing
unprovability from ZFC + V = L.

We will now present present Conservative Growth in four environments.

1. Graph Theory. This is the most rudimentary setting that we consider
. A graph is a G = (V,E), where E is an irreflexive symmetric relation
on V.
2. Model Theory. This is the most general setting that we consider.
The treatment is based on signatures SIG consisting of finitely many
constant and relation symbols, and equality. No function symbols.
3. Set Theory. Here the treatment takes into account very basic
elemental features of set theory based, as usual, on epsilon and
equality.
4. As Theories. Here we present section 3 in terms of a formal set theory.

In this first installment, we will only develop the theory through
TRIPLES. Pairs already leads to something interesting, but TRIPLES
gives us something truly unexpected.

1. GRAPH THEORY

IMPATIENT readers can skip to Definition 1.4 below, or even to section
2. Thus all of the material before Definition 1.4 can be viewed as
background.

We use G = (V,E) for graphs; i.e., E is an irreflexive symmetric
relation on the set V. E is the adjacency relation. ADJ(x) = {y: x,y
are adjacent}. We use V(G) for V and E(G) for E.

DEFINITION 1.1. G < G' if and only if G is an induced proper subgraph
of G'. In model theory, G < G' means that G is a proper substructure
of G'.

We apply the usual first order predicate calculus to any G. Here
parameters are allowed unless otherwise indicated. In particular, we
focus on the G definable subsets of V(G).

Do we allow equality in our treatment? We leave this ambiguous. The
results will be the same whether or not we allow equality.

NOTE: Can we give a nice treatment for graphs without using first
order predicate calculus? We are planning to take this matter up, more
generally, in a later posting on Mathematical Definability Theory.

DEFINITION 1.2. G <* G' if and only if G < G and every G definable
subset of V(G) is of the form ADJ(x) in G'.

THEOREM 1.1. <,<* are transitive. For all (countable) G there exists
(countable) G' such that G <* G'.

We now present conservative growth.

DEFINITION 1.3. G <** G' if and only if G <* G' and G is an elementary
substructure of G'.

Thus we are using the usual notion of elementary substructure from
model theory. I.e., any first order property in G of finitely many
vertices in G, holds, if and only if it holds in G'.

G has conservatively grown to G'. The growth is from <, the logical
growth is from <*. The conservative logical growth is from <**. We
have not had to change any truth values (involving vertices in G) when
growing from G to G'. Now that's progress (from G to G')!

THEOREM 1.2. There exists G <** G', G' countable. There exists G <**
G' <** G'', G'' countable.

THEOREM 1.3. Theorem 1.2 (both forms) is provably equivalent to
Con(Z_2) over WKL_0.

Thus we have seen that PAIRS - one single growth spurt - throws us out
of countable set theory.

We now come to TRIPLES. This is the result of two growth spurts.

The most obvious notion is simply G <** G' <** G''. This does not
break any new ground.

What we now want to do is compare (G,G') and (G',G''). We have grown
from (G,G') to (G',G''), as a consequence of growing from G to G' to
G''.

Since we are going to apply predicate calculus to (G,G') and (G',G''),
we had better be clear what (G,G') and (G',G'') is as a relational
structure.

DEFINITION 1.4. Let G < G'. (G,G') is the relational structure
(V(G'),E(G'),P), where P is V(G) as a unary predicate on V(G'). Thus
(G,G') is single sorted, with domain V(G'), and a binary and unary
relation.

DEFINITION 1.5. Let G,G',G'' be graphs. (G,G') <# (G',G'') if and only if
i. G <* G' <* G''.
ii Every first order statement that holds in (G,G') of given elements
of V(G), holds in (G',G'') of those elements of V(G).
It follows easily that G <** G' <** G''.

PROPOSITION 1.4. There exists countable graphs G,G',G'' such that
(G,G') <# (G',G'').

Proposition 1.4 is provable from large cardinals but not in ZFC.

THEOREM 1.5. Using Goedel's Completeness Theorem, Proposition 1.4 is
provably equivalent to a Pi01 sentence over WKL_0.

THEOREM 1.6. Proposition 1.4 is provably equivalent to Con(ZFC + the
scheme On is subtle) over WKL_0. Hence it is provable in ZFC + "there
exists a subtle cardinal", but not in ZFC (assuming ZFC is
consistent), and not in ZFC + "there exists a totally indescribable
cardinal" (assuming ZFC + "there exists a totally indescribable
cardinal" is consistent).

2. MODEL THEORY

DEFINITION 2.1. M definable always refers to first order predicate
calculus with or without equality, with parameters allowed. A subset
of dom(M) is atomically M definable if and only if it is M definable
by an atomic formula with at most one free variable and zero or more
parameters.

Do we allow equality in our treatment? We leave this ambiguous. The
results will be the same whether or not we allow equality.

Atomic definability is stronger than quantifier free definability, and
the difference is crucial. It is the difference between model theory
and set theory.

DEFINITION 2.2. Let M,M',M'' be structures in a finite language with
no function symbols. M < M' if and only if M is a proper substructure
of M'. M <* M' if and only if every M definable subset of dom(M) is
atomically M' definable. M <** M' if and only if M <* M' and M is an
elementary substructure of M'. (M,M') is M' with a unary relation
symbol for dom(M). (M,M') <# (M',M'') if and only if
i. M <* M' <* M''.
ii Every first order statement that holds in (M,M') of given elements
of dom(M), holds in (M',M'') of those elements of dom(M).
It follows easily that M <** M' <** M'

Note that Definition 2.2 has plenty of straightforward examples if we
use "quantifier free" instead of "atomically". E.g., set M =
(Q(0,1),<), M' = (Q(0,2),<), M'' = (Q(0,3),<). Then (M,M') <# (M',M'')
if we weaken atomic definability to quantifier free definability.

PROPOSITION 2.1. There exists countable structures M,M' such that M
<** M'There exists countable structures M,M',M'' such that M <** M'
<** M''.

PROPOSITION 2.2. There exists countable structures M,M',M'' such that
(M,M') <# (M',M'').

THEOREM 2.3. Using Goedel's Completeness Theorem, Propositions 2.1,
2.2 are provably equivalent to a Pi01 sentence over WKL_0.

THEOREM 2.4. Proposition 2.1 (both forms) is provably equivalent to
Con(Z_2) over WKL_0. Proposition 2.2 is provably equivalent to Con(ZFC
+ the scheme On is subtle) over WKL_0.

3. SET THEORY

We now formulate conservative growth in terms of models of set theory.

In this section, all structures M are based on a single binary
relation symbol epsilon. Our results are the same whether or not we
allow =.

We can proceed exactly as in section 2, treating M's as relational
structures as in section 2. Thus we have (M,M') <# (M',M'').

But instead, we will proceed in a way that conforms to very basic set
theoretic considerations. We will still proceed rather
minimalistically.

We still define M < M' as in section 2. We also use elementary
substructures as in section 2. Instead of the "atomic definability" in
section 2, or the use of ADJ(x) in section 1, we will conform to set
theory as follows.

DEFINITION 3.1. M <% M' if and only if M < M' and every M definable
subset of dom(M) is of the form {x: x epsilon a} where a is in dom(M')
and epsilon is the membership relation in M'. M <%% M' if and only if
M <# M' and M is an elementary substructure of M'.

DEFINITION 3.2. (M,M') <$ (M',M'') if and only if
i. M <% M' <% M''.
ii Every first order statement that holds in (M,M') of given elements
of dom(M), holds in (M',M'') of those elements of dom(M).
It follows easily that M <%% M' <%% M.''.

PROPOSITION 3.1. There exists countable structures M,M' such that M
<%% M'. There exists countable structures M,M',M'' such that M <%% M'
<%% M''.

PROPOSITION 3.2. There exists countable structures M,M',M'' such that
(M,M') <$ (M',M'').

THEOREM 3.3. Using Goedel's Completeness Theorem, Propositions 3.1,
2.2 are provably equivalent to a Pi01 sentence over WKL_0.

THEOREM 3.4. Proposition 3.1 (both forms) is provably equivalent to
Con(Z_2) over WKL_0. Proposition 3.2 is provably equivalent to Con(ZFC
+ the scheme On is subtle) over WKL_0.

4. AS THEORIES

We present a minimalistic formal system of high interpretation power
corresponding to TRIPLES. For readability, we give a semiformal
presentation, and require that the atomic definability be given by the
R predecessors.

We have only one binary relation symbol R, and two distinct unary
predicate symbols P,Q. We do not use equality.

1. P(x) implies Q(x).
2. Suppose all of the free variables in phi fall under P. (therexists
y)(Q(y) and (forall x)(x R y iff P(x) and phi^P), where x,y are
distinct, y does not appear in phi, and phi^P is the result of
relativizing all quantifiers in phi to P.
3. Suppose all of the free variables in phi fall under Q. (therexists
y)(forall x)(x R y iff Q(x) and phi^Q), where x,y are distinct, y does
not appear in phi, and phi^Q is the result of relativizing all
quantifiers in phi to Q
4. Let phi be a formula with all quantifiers relativized to P or to Q,
with no other occurrences of P,Q. Let phi* change the quantifiers
relativized to P to being relativized to Q, and unrelativize the
quantifiers relativized to Q. Assume all free variables in phi fall
under P. Then phi iff phi*.

THEOREM 4.1. The system 1-4 is mutually interpretable with ZFC + the
scheme "On is subtle" with respect to all first order formulas with
parameters. Thus the system 1-4 is interpretable in ZFC + "there
exists a subtle cardinal" and interprets ZFC + "there exists a totally
indescribable cardinal".

****************************************
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 547th 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

Harvey Friedman