[FOM] 651: Pi01 Incompleteness Update
Harvey Friedman
hmflogic at gmail.com
Tue Feb 2 07:58:44 EST 2016
There has been some considerable improvements in Pi01 Incompleteness,
both implicit Pi01 and explicit Pi01. These improvements are still
ongoing.
Here is a summary of where I am before giving details.
a. The lead implicitly Pi01 statement corresponds to SRP, and has
improved conceptually through use of embeddings, which are partial one
dimensional maps. Also I use inclusion maximal S^2 contained in R, and
don't have to take the root S. Both of these changes cut down on the
number of definitions - which was never too much for the lead
statement, but is now cut down much further.
b. The lead explicitly Pi01 statement corresponds to SRP, and is now
constructed as a very natural nondeterministic sequential
construction, in a rather common style, especially for anybody
involved in any kind of algorithmic mathematics or programming. There
is an unexpected bonus (this surfaced in earlier work) that the
setting is yet better than with a. In a, the space is Q[0,n]^k. In the
explicitly Pi01 statement the space is Q^k, and we can use the very
natural upper shift function, ush.
c. For the HUGE cardinal hierarchy, at this point it appears that the
best statement is going to be the explicitly Pi01 statement. It will
be more or less a refinement of b. We aim to make this refinement of b
as gentle as possible.
d. I see a,b stabilizing so that the urgent matter becomes writing up
the proofs for a,b. With c, I see some period of improvements,
converging with an explicitly Pi01 statement corresponding to HUGE,
which is a natural and simple variant of b. I hope to post on the
current state of the HUGE case in another week or so.
1. PRELIMINARIES
N is the set of all nonnegative integers, Q is the set of all
rationals. Q[0,n] is Q intersect [0,n]. We use i,j,k,n,m,r for
positive integers, and p,q for rationals.
R containedin Q[0,n]^k is order invariant if and only if for all order
equivalent x,y in Q[0,n]^k, x in R iff y in R.
Let S containedin Q[0,n]^k. S is embedded by h if and only if
i. h is a strictly increasing partial function from Q into Q.
ii. (x1,...,xk) in S iff (hx1,...,hxk) in S, provided both k-tuples
lie in Q[0,n]^k.
Thus we are using Q[0,n]^k as the ambient space.
THEOREM (immediate). Every R containedin Q[0,n]^k contains a maximal
S^2 containedin Q[0,n]^2k.
We need two more notion for section 3.
R containedin Q^k is order invariant if and only if for all order
equivalent x,y in Q^k, x in R iff y in R.
The upper shift of x in Q^k, written ush(x), results from adding 1 to
all nonnegative coordinates of x.
2. IMPLICITLY PI01 INCOMPLETENESS
PROPOSITION A. Every order invariant R containedin Q[0,n]^2k contains
a maximal S^2 containedin Q[0,n]^2k embedded by p if p < 0; p+1 if p
in N.
Proposition A can be seen to be implicitly Pi01 via the Goedel
Completeness Theorem.
THEOREM. Proposition A is independent of ZFC, and in fact provably
equivalent to Con(SRP) over WKL_0.
THEOREM. Proposition A is refutable in RCA_0 if we replace "if p in N"
by "otherwise".
INFORMAL IDEA: EVERY NICE SET HAS A MAXIMAL SQUARE WITH A NICE EMBEDDING.
3. EXPLICITLY Pi01 INCOMPLETENESS
Let R contaeinedin Q^2k. We present a nondeterministic procedure of
potentially infinite length. The ambition is to carry it out for
infinitely many steps. It will be clear from the procedure that you
can carry it out for infinitely many steps if and only if you can
carry it out for any finite number of steps.
We initialize with x1 = (0,...,k-1), and the pointer at x1. At any
stage in the process, we have x1,...,xr in Q^k, r varying, with the
pointer at some xi, 1 <= i <= r. We move to the next stage by
ii. (Expansion). Put all length k subsequences of the concatenation
x1x2...xr at the end of x1,...,xr, in any order, without repetitions.
iii. Move the pointer one position over to xi+1.
iii. Replacing xi by xi' which is either xi or has max(xi') < max(xi)
with {xi,xi'}^2 not contained in R.
Obviously by irreflexivity, we can always do this, taking xi' = xi.
But we impose the requirement that {x1,...,xi-1,xi'}^2 is contained in
R.
THEOREM (immediate, greedy). For all reflexive R containedin Q^2k, the
above nondeterministic construction can be carried out for infinitely
many steps - or equivalently, for any finite number of steps. We can
even require that all rationals that appear lie in {0,...,k-1}.
Now we make this more demanding, with one slight(?) change. Replace
{x1,...,xi-1,xi'}^2 containedin R
by
{x1,...,xi-1,ush(xi')}^2 containedin R.
THEOREM (easy). The following is false. Let R containedin Q^2k be
reflexive. This second nondeterministic construction can be carried
out for infinitely many steps - or equivalently, for any finite number
of steps.
PROPOSITION B. Let R containedin Q^2k be reflexive and order
invariant. This second nondeterministic construction can be carried
out for infinitely many steps - or equivalently, for any finite number
of steps.
Proposition B is obviously explicitly Pi01.
THEOREM. Proposition B is independent of ZFC, and in fact provably
equivalent to Con(SRP) over WKL_0.
**********************************************************
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 651st 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
Harvey Friedman
More information about the FOM
mailing list