[FOM] 659: Pi01 Incompleteness/SRP,HUGE/4
Harvey Friedman
hmflogic at gmail.com
Mon Feb 22 16:26:16 EST 2016
This posting will be restricted to three new developments:
1. A grammatical change in the lead statement designed to avoid all
possible ambiguities.
2. A new explicitly Pi01 statement arguably of roughly the quality of
the lead statement (which is implicitly Pi01 via the Goedel
Completeness Theorem).
3. A new implicitly Pi01 statement equivalent to Con(HUGE) that I like
better than previous such. It brings back the previous idea of "fixed
point minimizers".
4. A new explicitly Pi01 statement equivalent to Con(HUGE).
1. LEAD STATEMENT - GRAMMATICAL CHANGE
Recall the current form of the lead statement:
PROPOSITION. 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).
As mentioned before, there is a tiny ambiguity here. Is the S^2 merely
inclusion maximal, or is it also maximal with respect to the
additional embedding property?
Of course, I have made it clear that it is merely inclusion maximal.
But a creative use of English removes all ambiguity smoothly.
LEAD PROPOSITION. For all order invariant V containedin Q[0,n]^k, some
maximal S^2 containedin V is partially embedded by the function p if p
< 1; p+1 if p = 1,...,n-1.
Note that the Lead Proposition is implicitly Pi01 via the Goedel
Completeness Theorem.
I like the above English better, with the added advantage of no ambiguity.
Those interested in the ultimate level of detail should recall exactly
how I defined partial embeddings, as explained at the beginning of
http://www.cs.nyu.edu/pipermail/fom/2016-February/019510.html. The if
and only if is to work at vectors whose coordinates lie in the domain
of the partial embedding. We follow the usual convention in
mathematics that "an undefined term lies in a set" is always false.
2. LEAD FINITE STATEMENT
We now come to the new explicitly Pi01 statement. The form of the
statement is very simple.
LEAD FINITE PROPOSITION. For all order invariant V containedin
Q[0,n]^kr, some finitely maximal S^r containedin V is partially
embedded by the function p if p < 1; p+1 if p = 1,...,n-1.
LEAD FINITE PROPOSITION'. For all order invariant V containedin
Q[0,n]^kr, some finitely maximal S^r containedin V is partially
embedded by the function p if p < 1; p+1 if p in [1,n-1].
We have only to define finitely maximal. Recall that S^2 containedin V
is maximal if and only if every superset S'^2 containedin V is S^2.
DEFINITION 2.1. Let A,B containedin Q[0,n]^k. A,B are n-order
equivalent if and only if every element of A x {(0,...,n)} is order
equivalent to an element of B x {(0,...,n)} and vice versa.
DEFINITION 2.2. Let V containedin Q^kr. S^r containedin V is finitely
maximal if and only if S^r is finite, and every finite superset S'^r
containedin V is n-order equivalent to S^r.
It is easy to see that "finitely maximal" can be determined by an
effective procedure. t is also easy to give an explicit upper bound on
S in terms of the magnitudes of the numerators and denominators used
to present the coordinates of its elements. This puts the Lead Finite
Proposition in explicitly Pi01 form.
THEOREM 2.1. The Lead Finite Propositions are provably equivalent to
Con(SRP) over EFA.
3. FIXED POINT MINIMIZATION
DEFINITION 3.1. Let R containedin Q^2k. A fixed point minimizer for R
is a partial function f:Q^k into Q^k such that for all x in dom(f),
f(x) is the lexicographically least y = f(y) with x R y.
THEOREM 3.1. Let A containedin Q be well ordered. Every reflexive R
containedin Q^2k has a unique fixed point minimizer f:A^k into A^k.
PROPOSITION 3.2. Every reflexive order invariant R containedin Q^2k
has a fixed point minimizer f:A^k into A^k containing N^k, partially
embedded by the function p if p < 0; p+1 otherwise.
THEOREM 3.3. Proposition 3.2 is provably equivalent to Con(SRP) over WKL_0.
DEFINITION 3.2. Let R containedin Q^2k. A <= fixed point minimizer for
R is a partial function f:Q^k into Q^k such that for all increasing
(<=) x in dom(f), f(x) is the lexicographically least y = f(y) with x
R y.
PROPOSITION 3.4. Every reflexive order invariant R containedin Q^2k+2
has a <= fixed point minimizer f:A^k+1 into A^k+1 containing N^k
nontrivially embedded by the function union_n f_n...n|<n-1.
Here n ranges over positive integers, f_n...n is obtained by fixing
the first k-1 arguments to be n, |<n-1 restricts f_n...n to the domain
Q intersect (-infinity,n-1), and a nontrivial embedding of f:A^k+1
into A^k+1 is an embedding (as a function from A into A) which is not
the identity.
THEOREM 3.5. Proposition 3.2 is provably equivalent to Con(SRP) over
WKL_0. Proposition 3.4 is provably equivalent to Con(HUGE).
It is possible to reasonably go beyond HUGE, but at this point it is
not nearly as simple as simply union_n f_n...n|<n-1. HUGE is of course
big enuf to chew on.
There is a problem showing straightforwardly that Propositions 3.2 and
3.4 are implicitly Pi01 via the Goedel Completeness Theorem. The
problem arises from the use of lex. We can instead use lex' defined
by: x <lex' y if and only if max(x) < max(y) or (max(x) = max(y) and x
<lex y). Then Propositions 3.2 and 3.4 are implicitly Pi01 via the
Goedel Completeness Theorem, and Theorem 3.5 still holds.
4. FINITE FIXED POINT MINIMIZATION.
DEFINITION 3.1. Let R containedin Q^2k. An n-fixed point minimizer
for R is a finite fixed point minimizer f for R, where k-tuple drawn
from the union of {0,...,n}^k and the coordinates of the values of f
on {0,...,n}^k, lies in the domain of f. An n,<=-fixed point minimizer
for R is a finite <= fixed point minimizer f for R with this same
property.
PROPOSITION 3.1. Every reflexive order invariant R containedin Q^2k
has an n-fixed point minimizer partially embedded by the function p if
p < 0; p+1 if 0 <= p <= n.
PROPOSITION 3.2. Every reflexive order invariant R containedin Q^2k+2
has a <= n-fixed point minimizer partially embedded by the function
f_n...n|<n-1, which extends to p if p < 0; p+1 otherwise.
THEOREM 3.3. Proposition 3.1 is provably equivalent to Con(SRP) over
EFA. Proposition 3.2 is provably equivalent to Con(HUGE) over EFA.
These Propositions are explicitly Pi02. We can easily bound the
magnitudes of the denominators and numerators needed to put them in
explicitly Pi01 form.
**********************************************************
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 659th 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
656: Pi01 Incompleteness/SRP,HUGE/3 2/13/16 1:21PM
657: Definitional Complexity Theory 1 2/15/16 12:39AM
658: Definitional Complexity Theory 2 2/15/16 5:28AM
Harvey Friedman
More information about the FOM
mailing list