[FOM] 656: Pi01 Incompleteness/SRP,HUGE/3

Harvey Friedman hmflogic at gmail.com
Sat Feb 13 21:16:07 EST 2016 

I found a small bug in Definition 1.3 of
http://www.cs.nyu.edu/pipermail/fom/2016-February/019495.html  I wrote

DEFINITION 1.3. Let S containedin Q^k. S is partially embedded by h if
and only if
i. h is a partial function from Q into Q.
ii. For all x_1,...,x_k in Q, (x_1,...,x_k) in S iff (hx_1,...,hx_k) in S.

This should be

DEFINITION 1.3. Let S containedin Q^k. S is partially embedded by h if
and only if
i. h is a partial function from Q into Q.
ii. For all x_1,...,x_k in dom(h), (x_1,...,x_k) in S iff (hx_1,...,hx_k) in S.

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

There is a reasonably good way of going from the lead implicitly Pi01 statement

PROPOSITION 2.1. Every order invariant V containedin Q[0,n]^k contains
a maximal S^2, partially embedded by the function p if p < 1; p+1 if p
in {1,...,n-1}.

to an explicitly Pi01 form, which is provably equivalent to
Proposition 2.1 over WKL_0 (and hence to Con(SRP)). This way uses
heights.

We again summarize our inventory of Pi01 Incompleteness.

1. The lead statement. This is implicitly Pi01, and easy to see
provably equivalent to a Pi01 sentence via the Goedel Completeness
Theorem:

PROPOSITION 2.1. Every order invariant V containedin Q[0,n]^k contains
a maximal S^2, partially embedded by the function p if p < 1; p+1 if p
in {1,...,n-1}.

Provably equivalent to Con(SRP).

2. The new lead explicitly Pi01 statement in rational vectors,
presented here below, using heights.

3. A second explicitly Pi01 statement in rational vectors. This has
the advantage of leading to 4 below.

PROPOSITION 3.2. In every order invariant R containedin Q^2k,
{0,...,k}^k has a finite basis B with a finite basis C containing B
and ush(C), both of height at most (8k)!.

Provably equivalent to Con(SRP) over EFA.

The statement is of course shorter without the height estimate, which
can also be inferred.

4. A third explicitly Pi01 statement in rationals vectors, that is a
very strong extension using a side condition.

PROPOSITION 4.2. In every order invariant R containedin Q^2k,
{0,...,2k}^k has a finite <= basis B with a finite <= basis C containing B
and ush(C), both of height at most (8k)!, where C_k+.5|<=k = ush(C)_k|<=k.

Provably equivalent to Con(HUGE) over EFA.

The statement is of course shorter without the height estimate, which
can also be inferred.

5. A fourth explicitly Pi01 statement  in the positive integers.

PROPOSITION 5.3. For all piecewise linear V containedin Z+^k over
{-k,...,k}, {8k,...,n}! has a V basic cover with a V basic cover below
(n+1)!.

Provably equivalent to Con(MAH) over ACA.

The statement is of course shorter without the estimate, which can
also be inferred.

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

Now for the new lead explicitly Pi01 statement. (item 2 above).

DEFINITION 6.1. Let x in Q^k. The height of x, hgt(x), is the maximum
of the magnitudes of the numerators and denominators of all
coordinates of x, when put in reduced form. Let S containedin Q^k.
hgt(S) is the maximum of the heights of the elements of S.

DEFINITION 6.2. Let V containedin Q[0,n]^k. An (r,s)-maximal S^2 in V
is an S^2 containedin V, where for all hgt(x) <= r in Q[0,n]^k\S,
there exists hgt(y) <= s in S, with {x,y}^2 notcontainedin V. An
(r_1,s_1),...,(r_t,s_t)-maximal S^2 in V is a simultaneously
(r_1,s_1)-maximal,...,(r_t,s_t)-maximal S^2 in V.

THEOREM 6.1. Every order invariant V containedin Q[0,k]^k contains a
finite (k,(8k)!)-maximal S^2, partially embedded by the function p if
p < 1; p+1 if p in {1,...,k-1}.

PROPOSITION 6.2. Every order invariant V containedin Q[0,k]^k contains
a finite (k,(8k)!),((8k)!,(8k)!!)-maximal S^2, partially embedded by
the function p if p < 1; p+1 if p in {1,...,k-1}.

PROPOSITION 6.3. Every order invariant V containedin Q[0,k]^k contains
a (k,(8k)!),((8k)!,(8k)!!)-maximal S^2 of height <= (8k)!!, partially
embedded by the function p if p < 1; p+1 if p in {1,...,k-1}.

THEOREM 6.4. Theorem 6.1 is provable in EFA. Propositions 6.2, 6.3 are
provably equivalent to Con(SRP) over EFA.

Here EFA = exponential function arithmetic.

**********************************************************
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 656th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM
640: Progress in Pi01 Incompleteness 3  10/30/15  2:30PM
641: Progress in Pi01 Incompleteness 4  10/31/15  8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1  11/3/15  11:57PM
644: Fixed Point Selectors 1  11/16/15  8:38AM
645: Fixed Point Minimizers #1  11/22/15  7:46PM
646: Philosophy of Incompleteness 1  Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1  11/30/15  6:52PM
648: Necessary Irrelevance 1  12/21/15  4:01AM
649: Necessary Irrelevance 2  12/21/15  8:53PM
650: Necessary Irrelevance 3  12/24/15  2:42AM
651: Pi01 Incompleteness Update  2/2/16  7:58AM
652: Pi01 Incompleteness Update/2  2/7/16  10:06PM
653: Pi01 Incompleteness/SRP,HUGE  2/8/16  3:20PM
654: Theory Inspired by Automated Proving 1  2/11/16  2:55AM
655: Pi01 Incompleteness/SRP,HUGE/2  2/12/16  11:40PM

Harvey Friedman

More information about the FOM mailing list