# [FOM] 258:Pi01/simplification/restatement

Harvey Friedman friedman at math.ohio-state.edu
Sun Nov 27 02:12:36 EST 2005

We now have some simplifications.

We now use R containedin [1,n]k x [1,n]k = [1,n]2k, instead of the previous
R containedin [1,n]3k x [1,n]k. This move supports the terminology "for all
strictly dominating order invariant R containedin [1,n]2k". There is a small
cost to doing this, but it is well worth it: we must use RRRR[A'\(8k)!],
RRRR[A'], RRRA, instead of RR<A'\(8k)!>, RR<A'>, R<A>. However, once we are
using iterated R's, we might as well use more iterated R's.

Another simplification arises when using antichain terminology. Under this
approach, we only use two sets, and inclusion with respect to k tuples of
powers of (8k)!+1.

Below we first present the statement using antichains, since the statement
is simpler. Since R containedin [1,n]k x [1,n]k can be viewed as a graph
whose vertex set is [1,n]k, and iterated R's correspond to paths, the
statement has a graph theoretic flavor. We also sense algebraic overtones.

The second presentation is like the previous Proposition A, which is more
closely allied to fixed points, rather than graph theory.

We have versions that correspond to the huge cardinal hierarchy. However, at
present, these impose a side condition on A which is digestible but
definitely not beautiful.

#########################################

Pi01 INCOMPLETENESS 2
by
Harvey M. Friedman
November 27, 2005

NOTE: This supercedes Pi01 Incompleteness 1, November 10, 2005, and FOM
postings 254-257.

"Beautiful" is a word used by mathematicians with a semi rigorous meaning.

We give "arguably beautiful" explicitly Pi01 sentences independent of ZFC.
See Proposition A from section 1 and Proposition B from section 2, and
variants.

Proposition A is simplest and has a graph theoretic flavor, with algebraic
overtones. Proposition B has a fixed point flavor.

1. Pi01 INDEPENDENT STATEMENTS USING ANTICHAINS.

Let A containedin [1,n]k. We write A' = [1,n]k\A. This treats [1,n]k as the
ambient space.

Let R containedin [1,n]2k. We define

RA = R[A] = {y in [1,n]k: (therexists x in A)(R(x,y))}.

We say that R is strictly dominating if and only if for all x,y in
[1,n]k, if R(x,y) then max(x) < max(y).

THEOREM 1.1. For all k,n >= 1 and strictly dominating R containedin ]1,n]2k,
there exists A containedin [1,n]k such that RA = A'. Furthermore, A
containedin [1,n]k is unique.

For A containedin [1,n]k and t >= 1, we write A\t = {x in A: t is not a
coordinate of x} = "A with t omitted".

Here is a modification of Theorem 1.1 which we call the "complementation
theorem for R[A\(8k)!]".

THEOREM 1.2. For all k,n >= 1 and strictly dominating R containedin [1,n]2k,
there exists A containedin [1,n]k such that R[A\(8k)!] = A'. Furthermore, A
containedin [1,n]k is unique.

We now incorporate the antichain concept.

Let R containedin [1,n]2k. We say that A is an antichain for R if and only
if A containedin [1,n]k and A,RA are disjoint.

Of course, we have the following "maximal antichain" theorem.

THEOREM 1.3. For all k,n >= 1, every R containedin [1,n]2k has a maximal
antichain.

Note that Theorem 1.3 is virtually contentless, since we are in a finite
context where every nonempty class has a maximal element.

Note that Theorem 1.1 provides a much stronger kind of antichain, which we
call a "complete" antichain. We refer to the following as a "complete
antichain" theorem.

THEOREM 1.4. For all k,n >= 1, every strictly dominating R containedin
[1,n]2k has an antichain A such that RA contains A'. Furthermore, A is
unique.

However, the analog of Theorem 1.4 for R[A\(8k)!] is false.

THEOREM 1.5. The following is false. For all k,n >= 1, every strictly
dominating R containedin [1,n]2k has an antichain A such that R[A\(8k)!]
contains A'.

We will weaken the conclusion in a simple way.

Our development depends heavily on a very strong regularity condition on R.

We say that R containedin [1,n]k is order invariant if and only if
for all x,y in [1,n]k of the same order type, R(x) iff R(y). The number of
such R is bounded by an exponential expression in k that does not depend on
n.

The imposition of order invariance is still not sufficient:

THEOREM 1.6. The following is false. For all k,n >= 1, every strictly
dominating order invariant R containedin [1,n]2k has an antichain A such
that R[A\(8k)!] contains A'.

However, we can assert that R[A\(8k)!] contains a "significant part" of A'
as follows.

The powers of t are the numbers t^i, i >= 0.

THEOREM 1.7. For all k,n >= 1, every strictly dominating order invariant R
containedin [1,n]2k has an antichain A such that R[A\(8k)!] contains all k
tuples of powers of (8k)!+1, lying in A'.

Obviously we can apply R once or more times to both sides of the equations
in Theorems 1.1 and 1.2, and to both sides of the containments in Theorems
1.3 and 1.7. This is because, e.g.,

RRRRA = RRR[A']
RRRR[A\(8k)!] = RRR[A']
RRRRA contains RRR[A']

RA = A'
R[A\(8k)!] = A'
RA contains A'

respectively. However,

RRRR[A\(8k)!] contains all k tuples of powers of (8k)!+1, lying in RRR[A']

R[A\(8k)!] contains all k tuples of powers of (8k)!+1, lying in A'.

The use of p R's has an obvious graph theoretic interpretation: paths in R
(viewed as a graph) of length p.

So what happens?

PROPOSITION A. For all k,n >= 1, every strictly dominating order invariant R
containedin [1,n]2k has an antichain A such that RRRR[A\(8k)!] contains all
k tuples of powers of (8k)!+1, lying in RRR[A'].

Proposition A is obviously an explicitly Pi01 sentence. It is independent of
ZFC. Here is much more precise information.

Let MAH = ZFC + {there exists a strongly n-Mahlo cardinal}_n. Let MAH+ = ZFC
+ "for all n there exists a strongly n-Mahlo cardinal".

THEOREM 1.8. MAH+ proves Proposition A. However, Proposition A is not
provable in any consistent fragment of MAH that derives Z = Zermelo set
theory. In particular, Proposition A is not provable in ZFC, provided ZFC is
consistent. These facts are provable in RCA0.

THEOREM 1.9. It is provable in ACA that Proposition A is equivalent to
Con(MAH).

There are some variants of Proposition A which have the same status (as
given by Theorems 1.8 and 1.9).

a. We can use more R's in the two expressions, as long as the first uses
exactly one more than the second, and the first uses at least 4 R's. When
the number of R's get substantial relative to k, we have to raise (8k)!.

b. We can use t instead of (8k)!, and hypothesize that t is at least (8k)!.
The use of (8k)! is merely safe and convenient, and not anything near
optimal.

c. In A\(8k)!, we are eliminating all vectors in which (8k)! appear. We can
instead only eliminate a single vector. In particular, we can just eliminate
the k tuple ((8k)!,...,(8k)!). Thus we can replace A'\(8k)! with A\{(8k)!}k.
Of course, this weakens the statement and is also not so pretty. But the
idea behind A\(8k)! is that we are perturbing A just a little bit. With
A\{8k)!}k, we are perturbing A' by even less, so there is something to be
said for this modification.

d. We can combine some or even all of a - d.

Note that Theorems 1.3 - 1.7 and Proposition A have an obvious graph
theoretic flavor, with lattice points as the vertex set.

2. Pi01 INDEPENDENT STATEMENTS WITHOUT USING ANTICHAINS.

Here we avoid using antichains, and instead emphasize the fixed point
aspects.

We start with the basic unique fixed point theorem for the operator R[A'].

THEOREM 2.1. For all k,n >= 1 and strictly dominating R containedin ]1,n]2k,
there exists A containedin [1,n]k such that R[A'] = A. Furthermore, A
containedin [1,n]k is unique.

The "omission" operator R[A'\(8k)!] also has a unique fixed point.

THEOREM 2.2. For all k,n >= 1 and strictly dominating R containedin [1,n]2k,
there exists A containedin [1,n]k such that R[A'\(8k)!] = A. Furthermore, A
containedin [1,n]k is unique.

However, we can't get a COMMON fixed point

R[A'\(8k)!] = R[A'] = A.

THEOREM 2.3. The following is false. For all k,n >= 1 and strictly
dominating R containedin [1,n]3k x [1,n]k, there exists A containedin [1,n]k
such that R[A'\(8k)!] = R[A'] = A.

We will weaken this three term common fixed point equation so that it is
attainable. The weakening involves replacing = both with containedin and
with "having the same elements of a certain kind".

Order invariance will not be sufficient:

THEOREM 2.4. The following is false. For all k,n >= 1 and strictly
dominating order invariant R containedin [1,n]3k x [1,n]k, there exists A
containedin [1,n]k such that R[A'\(8k)!] = R[A'] = A.

The powers of t are the numbers t^i, i >= 0.

THEOREM 2.5. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that the three
sets R[A'\(8k)!] containedin R[A'] containedin A contain the same
k tuples of powers of (8k)!+1.

Obviously we can apply R once or more times to both sides of the equations
in Theorems 2.1 and 2.2. This is because, e.g.,

RRRR[A'] = RRRA
RRRR[A'\(8k)!] = RRRA

R[A'] = A
R[A'\(8k)!] = A

What happens if we apply R, once or more, to the expressions in the three
term tower of Theorem 2.5?

Again

1) RRRR[A'\(8k)!] containedin RRRR[A'] containedin RRRA

follows immediately from

2) R[A'\(8k)!] containedin R[A'] containedin A.

However,

"the three sets in 1) above contain the same k tuples of powers of
(8k)!+1"

"the three sets in 2) above contain the same k tuples of powers of
(8k)!+1."

PROPOSITION B. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that the three
sets RRRR[A'\(8k)!] containedin RRRR[A'] containedin RRRA contain the
same k tuples of powers of (8k)!+1.

Proposition B is obviously an explicitly Pi01 sentence. It is independent of
ZFC. Here is much more precise information.

Let MAH = ZFC + {there exists a strongly n-Mahlo cardinal}_n. Let MAH+ = ZFC
+ "for all n there exists a strongly n-Mahlo cardinal".

THEOREM 2.6. MAH+ proves Proposition A. However, Proposition B is not
provable in any consistent fragment of MAH that derives Z = Zermelo set
theory. In particular, Proposition A is not provable in ZFC, provided ZFC is
consistent. These facts are provable in RCA0.

THEOREM 2.7. It is provable in ACA that Proposition B is equivalent to
Con(MAH).

There are some variants of Proposition B which have the same status (as
given by Theorems 2.6 and 2.7).

a. We can use more R's in the three expressions, as long as the first two
use the same number of R's, with at least 4 R's, and the third uses one
fewer. When the number of R's get substantial relative to k, we have to
raise (8k)!.

b. We can use t instead of (8k)!, and hypothesize that t is at least (8k)!.
The use of (8k)! is merely safe and convenient, and not anything near
optimal.

c. We can eliminate a single vector instead of all vectors in which (8k)!.
Thus we can replace A'\(8k)! with A'\{(8k)!}k. Of course, this weakens the
statement and is also not so pretty. But the idea behind A'\(8k)! is that we
are perturbing A' just a little bit. With A'\{8k)!}k, we are perturbing A'
by even less, so there is something to be said for this modification.

d. We can combine some or even all of a - d.

3. CONTROLLING PROPOSITION A.

We wish to control the strength of Propositions A,B by weakening them in
simple ways. This seems to be a large subject, with much to work out, and we
merely scratch the surface of it here.

PROPOSITION A1. For all k,n >= 1, every strictly dominating order invariant
R containedin [1,n]2k has an antichain A such that RRRR[A\(8k)!] contains
all k tuples from the first 3 powers of (8k)!+1, lying in RRR[A'].

PROPOSITION A2. For all k,n >= 1, every strictly dominating order invariant
R containedin [1,n]2k has an antichain A such that RRRR[A\(8k)!] contains
all k tuples from the first k powers of (8k)!+1, lying in RRR[A'].

PROPOSITION A3. For all k,n >= 1, every strictly dominating order invariant
R containedin [1,n]2k has an antichain A such that RRRR[A\(8k)!] contains
all k tuples from the first (8k)! powers of (8k)!+1, lying in RRR[A'].

PROPOSITION A4. For all k,n >= 1, every strictly dominating order invariant
R containedin [1,n]2k has an antichain A such that RRRR[A\(8k)!] contains
all k tuples from 1,(8k)!+1,...,(8k)!+p, lying in RRR[A'].

THEOREM 3.1. Propositions A1,A2,A4 are provable in ACA but not in PA. It is
provable in PRA that Propositions A1,A2,A4 are equivalent to Con(PA).

THEOREM 3.2. For fixed p, Proposition A4 is provable in PA. The set of
Propositions obtained by fixing p in Proposition A4 is equivalent, over PRA,
to Con(PA). For fixed p, Proposition A4 requires approximately p quantifier
induction (exact calculation is being postponed).

THEOREM 3.3. Proposition A3 is provable in Z but not in WZC. It is provable
in PRA that Proposition A3 is equivalent to Con(WZ).

Here Z = Zermelo set theory, and WZC = Zermelo set theory with only bounded
separation, with the axiom of choice. The equivalence of Con(WZC) and the
consistently of Russell's type theory with infinity is provable in PRA.

4. CONTROLLING PROPOSITION B.

We wish to control the strength of Proposition B by weakening it in simple
ways. This seems to be a large subject, with much to work out, and we merely
scratch the surface of it here.

PROPOSITION B1. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from the first three powers of (8k)!+1.

PROPOSITION B2. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from the first k powers of (8k)!+1.

PROPOSITION B3. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from the first (8k)! powers of (8k)!+1.

PROPOSITION B4. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exist A containedin [1,n]k such that the
three sets RR<A'\(8k)!> containedin RR<A'> containedin RA contain the same k
tuples from 1,(8k)!+1,...,(8k)!+p.

THEOREM 4.1. Propositions B1,B2,B4 are provable in ACA but not in PA. It is
provable in PRA that Propositions B1,B2,B4 are equivalent to Con(PA).

THEOREM 4.2. For fixed p, Proposition B4 is provable in PA. The set of
Propositions obtained by fixing p in Proposition B4 is equivalent, over PRA,
to Con(PA). For fixed p, Proposition B4 requires approximately p quantifier
induction (exact calculation is being postponed).

THEOREM 4.3. Proposition B3 is provable in Z but not in WZC. It is provable
in PRA that Proposition B3 is equivalent to Con(WZ).

It looks like I forgot to mention Theorem 4.3 in posting #255.

5. FIT, CLASSIFICATIONS.

We can take a general view of Proposition B and place it in a theory called
FIT = finite inclusion theory.

Let us begin by recalling

THEOREM 2.5. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that
the three sets R[A'\(8k)!] containedin R[A'] containedin A contain the same
k tuples of powers of (8k)!+1.

We begin our classification theory by considering all three expressions
appearing in Theorem 2.4.

A
R[A']
R[A'\(8k)!]

Theorem 2.5 uses these two inclusion statements.

s containedin t
s containedin* t

where s,t are among the above five expressions. Here s ontainedin* t means
that every k tuple of powers of (8k)! lying in s, also lies in t.

Thus we can rewrite Theorem 2.5 as follows.

THEOREM 2.5'. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that
1. R[A'] containedin A.
2. A containedin* R[A'\(8k)!].

Note how the conclusion of Theorem 2.5 reduces to only two inclusions. This
is because

R[A'\(8k)!] containedin R[A'] containedin A
R[A'\(8k)!] =* R[A'] =* A

follow trivially from 1,2 in Theorem 2.5'.

Let K1 be the set of all inclusion statements of the above form. K1 has 18
elements, six of which are trivial because their left and right sides are
identical. So there are really 12 elements of K1 that need to be considered.

We now wish to classify (i.e., determine the truth or falsity of) all
statements of the following form.

TEMPLATE K1. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]3k x [1,n]k, there exists A containedin [1,n]k such that a
given subset of K1 holds conjunctively.

There are 2^12 subsets of K1 that need to be considered, which is 4096.

We have been able to carry out this classification; i.e., determine the
truth values of all instances of Template K1.

Now what exactly does this mean?

For one thing, we can actually exhibit this table, since 4096 is not too
big.

But we have a methodology for determining these truth values without
exhibiting the entire table. Instead, we use a tree like methodology which
does exhibit all of the maximal subsets of K1 for which Template K1 holds.

The fundamental finding that can be stated without exhibiting anything is:

THEOREM 5.1. Every instance of Template K1 is provable or refutable in EFA
(exponential function arithmetic).

In the course of this analysis, we did discover a variant of Theorem 2.5
that does not seem to follow formally from Theorem 2.5, or formally imply
Theorem 2.5:

THEOREM 2.5*. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that the three
sets A containedin R[A'\(8k)!] containedin R[A'] contain the same k tuples
of powers of (8k)!+1.

We also discovered an interesting counterexample.

THEOREM 5.2. The following is false. For all k,n >= 1 and strictly
dominating order invariant R containedin [1,n]2k, there exists A containedin
[1,n]k such that R<A'\(8k)!> containedin A containedin R<A'> and R[A']
containedin* R[A'\(8k)!].

Now recall

PROPOSITION B. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exist A containedin [1,n]k such that the three
sets RRRR[A'\(8k)!] containedin RRRR[A'] containedin RRRA contain the same k
tuples of powers of (8k)!+1.

We analogously considering all three expressions appearing in Proposition B.

RRRA
RRRR[A']
RRRR[A'\(8k)!]

Proposition A uses these two inclusion statements.

s containedin t
s containedin* t

where s,t are among the above five expressions. Here s ontainedin* t means
that every k tuple of powers of (8k)! lying in s, also lies in t.

Thus we can rewrite Proposition B as follows.

PROPOSITION B'. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that
1. RRRR[A'] containedin RRRA.
2. RRRA containedin* RRRR[A'\(8k)!].

Note how the conclusion of Theorem 2.4 reduces to only two inclusions. This
is because

RRRR[A'\(8k)!] containedin RRRR[A'] containedin RRRA
RRRR[A'\(8k)!] =* RRRR[A'] =* RRRA

follow trivially from 1,2 in Proposition B'.

Let K2 be the set of all inclusion statements of the above form. K2 has 18
elements, six of which are trivial because their left and right sides are
identical. So there are really 12 elements of K2 that need to be considered.

We now wish to classify (i.e., determine the truth or falsity of) all
statements of the following form.

TEMPLATE K2. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that a given
subset of K2 holds conjunctively.

There are 2^12 subsets of K2 that need to be considered, which is 4096.

THEOREM 5.3. Every instance of Template K2 can be proved or refuted in MAH+.
In fact, every instance of Template K2 is either

i. Provable in EFA, or
ii. Refutable in EFA, or
iii. Provably equivalent, over ACA, to Con(MAH).

We have discovered a variant of Proposition B that does not seem to
formally imply or be implied by Proposition B:

PROPOSITION B*. For all k,n >= 1 and strictly dominating order invariant R
containedin [1,n]2k, there exists A containedin [1,n]k such that the three
sets RRRA containedin RRRR[A'\(8k)!] containedin RRRR[A'] contain the same k
tuples of powers of (8k)!+1.

Proposition B* is also provably equivalent, over ACA, to Con(MAH).

It is more ambitious to work with the five expressions

A
A'
RA
R[A']
R[A'\(8k)!].

And the two inclusion relations

s containedin t
s containedin* t.

This comprises 50 inclusions. The idea is to classify Proposition B using,
as conclusion, any of the 2^50 subsets interpreted conjunctively. I.e.,
which are true and which are false, and show that each one can be decided
in, say, EFA.

Getting rid of silly inclusions, we have 40 inclusions, and 2^40 subsets.
This is roughly 1 trillion statements.

Yet more ambitiously, we can generate a hierarchy of expressions as follows.

1. A,A',A\(8k)!,A'\(8k)! are expressions.
2. If t is an expression, then so are Rt, (Rt)', (Rt)\(8k)!, (Rt)'\(8k)!.

Atomic statements are again of the forms

3. s containedin t.
4. s containedin* t.

We want to handle arbitrary finite sets of atomic statements, interpreted
conjunctively.

At the level appropriate for Theorem 1.4, we have 4 expressions from 1 and
another 16 from 2, for a total of 20 expressions. This yields 2(20)(19) =
760 nontrivial inclusions. The number of statements to be analyzed is 2^760.

At the level appropriate for Proposition B, we have 4 expressions from 1, 16
more from one application of 2, and 64 more from a second application of 2,
256 more from a third application of 2, and 1024 more from a fourth
application of 2. The total number of expressions is 1300, yielding
2(1300)(1299) = 3,377,400 nontrivial inclusions. The number of statements to
be analyzed is 2^3,377,400.

It remains to be seen whether these classifications can actually be carried
out, and whether EFA is enough for the 2^760 classification, and whether
Con(MAH) is enough for the 2^3,377,400 classification. Expect massive
amounts of silly trivialities. The problem is to tame what's left.

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

manuscripts. This is the 258th 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM

Harvey Friedman