[FOM] 557: New Pi01

Harvey Friedman hmflogic at gmail.com
Thu Oct 30 14:05:20 EDT 2014

We have what I regard as a strong new development in Pi01
incompleteness, particularly from the combinatorial standpoint. Here
are some new virtues.

1. I use order invariant binary relations on N^k and {0,...,t}^k,
instead of Q^k. The first version does not even use order invariance.
2. There are no sections and no maximality.
3. Instead of sections and maximality, we use reductions of one vector
to another.
4. The transition to finite forms is immediate.

I definitely had traces of these ideas already in the present version
84. Flat Mental Pictures, September 5, 2014, 5 pages. Extended abstract.

DEFINITION 1. Let R be contained in N^2k = N^k x N^k. x reduces to y
if and only if x R y and max(x) > max(y). S is irreducible in R if and
only if S containedin N^k and no element of S reduces to any element
of S. S is a basis if and only if S is irreducible and every element
of N^k\S reduces to an element of S. For A containedin N, A! = {n!: n
in A}.

THEOREM 1.  Every R containedin N^2k has a unique basis S.

DEFINITION 2 . Let R containedin N^2k. A_1 red ... red A_r for S if and only if
i. S containedin N^k.
ii. A_1,...,A_r are subsets of N.
iii. Every element of  (A_i + {0,1})^k, i < r, in N^k\S, reduces to an
element of A_i+1 intersect S.

THEOREM 2 (trivial). Let R containedin N^2k and S be irreducible. The
following are equivalent.
i. N red N for S.
ii. N red S for S.
iii. N\S red N for S.
iv. N\S red S for S.
v. S is a basis.

PROPOSITION 1. Every R containedin N^2k has an irreducible set for
which some A red B red N\(A-1), A infinite.

PROPOSITION 2. Every order invariant R containedin N^2k has an
irreducible set for which some A red B red N\(A-1), A infinite.

PROPOSITION 3. Every order invariant R containedin N^2k has an
irreducible set for which some A red B red N\(A-1), A = (8kN)!.

We now use the obvious analog of Definitions 1,2 for order invariant R
containedin {0,...,t}^2n.

DEFINITION 3. For t in N, [t] = {0,...,t}. We repeat Definitions 1,2
with N replaced by [t].

PROPOSITION 4. Every order invariant R containedin [t]^2k has an
irreducible set for which some  A red B red [t]\(A-1), where A =
(8kN)! intersect [t].

Note that Proposition 4 is explicitly Pi01.

THEOREM 5. Propositions 1-4 are provably equivalent to Con(SMAH) over
ACA. SMAH is the strongly Mahlo cardinal hierarchy.

My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
This is the 557th 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

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
554: Foundational Methodology 5/Maximality  10/26/14 3:17AM
555: Foundational Methodology 6/Maximality  10/29/14 12:32PM
556: Flat Foundations 1  10/29/14  4:07PM

Harvey Friedman

More information about the FOM mailing list