[FOM] 260:Pi01/simplification

[Harvey Friedman]

I introduce a new Pi01 statement which, overall, seems better than all
others. I have obtained some feedback from mathematicians outside logic to
confirm my impression.

Nevertheless, the situation is not completely obvious, so I will retain the
statements pointed to in posting #259, as presented in posting #258.

The upshot is that on my website at

http://www.math.ohio-state.edu/%7Efriedman/

under downloadable manuscripts, manuscript number 49, you will find two pdf
files. The first is the old November 30, 2005 file, unchanged. The second
file is dated December 3, 2005, and is shorter, as it focuses only on the
new version, which I now discuss.

Recall

OLD 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'].

For the new version, we use a squashing operation. We use log for the base 2
logarithm, and flog for the floor of the log. We extend flog coordinatewise
to elements of [1,n]k. For A containedin [1,n]k, we define

flog A = flog[A]. 

Thus flog "squashes" A.

NEW THEOREM 1.4. For all k,n >= 1, every strictly dominating order invariant
R containedin [1,n]2k has an antichain A such that flog R[A\2^(8k)!-1]
contains flog A'.

NEW PROPOSITION A. For all k,n >= 1, every strictly dominating order
invariant R containedin [1,n]2k has an antichain A such that flog
RRRR[A\2^(8k)!-1] contains flog RRR[A'].

Here 2^(8k)!-1 is 

1 less than 2 to the power (8k)!.

Again, this is just a convenient expression that is a big enough power of 2,
minus 1. 

Again, new A is independent of ZFC, and is provably equivalent, over ACA, to
the consistency of MAH.

In order to tame the statement, so that it corresponds to, say, PA and WZC,
as before, we put n to be various expressions in k.

NEW PROPOSITION A1. For all k >= 1, every strictly dominating order
invariant R containedin [1,2^((8k)!+3)]2k has an antichain A such that flog
RRRR[A\2^(8k)!-1] contains flog RRR[A'].

NEW PROPOSITION A2. For all k >= 1, every strictly dominating order
invariant R containedin [1,(8k)!!!]2k has an antichain A such that flog
RRRR[A\2^(8k)!-1] contains flog RRR[A'].

The first is provably equivalent, over PRA, to Con(PA). The second is
provably equivalent, over EFA, to Con(WZC).

We don't have time now to carry out the corresponding classification theory,
which should be quite similar to that carried out previously in the 11/30/05
manuscript. For the new Theorem 1.4, it will involve the expressions

RA
A'
flog R[A\2^(8k)!-1]
flog A'

under inclusion. 

It is natural to extend this to:

A
A'
RA
R[A']
A\2^(8k)!-1
A'\2^(8k)!-1
R[A\2^(8k)!-1]
R[A'\2^(8k)!-1]
flog's of the above

under inclusion. The conjecture is always that the resulting statements are
provable or refutable in EFA.

For the new Proposition 1.4, it will involve the expressions

RA
A'
flog RRRR[A\2^(8k)!-1]
flog RRR[A']

under inclusion.

It is natural to consider various larger classes of expressions. The
conjecture is that the resulting statements are

1. Provable in EFA; or
2. Refutable in EFA; or
3. Provably equivalent, in ACA, to Con(MAH).

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 259th 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
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM

Harvey Friedman