894: Update on Tangible Incompleteness/2
Harvey Friedman
hmflogic at gmail.com
Sat Sep 25 02:51:13 EDT 2021
We begin with some modifications of 890.
MODIFICATIONS OF 890,
https://cs.nyu.edu/pipermail/fom/2021-September/022870.html Con(SRP)
We wrote:
"As before, the first refresh is by default considered to be B_1 =
{0,t,2t,...,nt}^k. Each succeeding refresh B_i+1 is the usual
fld(A_i)^k but with only the k-tuples whose max is smaller than the
largest integer appearing in the previous refresh B_i. Thus the
largest
number appearing in these successive refreshes are now strictly decreasing."
New version for ALG(t,k,n,R)./2:
"We define A_i,B_i for all i until we reach |B_i| = 1, and then we stop.
Set A_1 = emptyset and B_1 = {0,t,2t,...,nt}^k.
case 1. B_i = emptyset. Let j be greatest j < i and B_j-1 = emptyset
if j exists; j = 1 otherwise; B_i+1 consists of the elements of
fld(A_i)^k whose max is less than the max of some element of B_j.
A_i+1 = A_i.
case 2. B_i is not empty. Choose u in B_i and some x such that not x
R u and max(x) <= max(u). Set B_i+1 = B_i \ {u} and A_i+1 = A_i union
{x,ush(x;t)}."
1. TWO LEAD STATEMENTS FOR MATHEMATICIANS - no change SEE
https://cs.nyu.edu/pipermail/fom/2021-September/022870.html Con(SRP)
2. FIRST NONDETERMINISTIC ALGORITHM - Pi01 incompleteness SEE
https://cs.nyu.edu/pipermail/fom/2021-September/022870.html Con(SRP)
3. SECOND NONDETERMINISTIC ALGORITHM - Pi02 incompleteness SEE
https://cs.nyu.edu/pipermail/fom/2021-September/022870.html Con(SRP)
4. THIRD NONDETERMINISTIC ALGORITHM - PREPARATION
5. THIRD NONDETERMINISTIC ALGORITHM - Pi01 incompleteness Con(HUGE)
We now come to the main focus of this posting which is refining 890
for HUGE instead of SRP.
4. THIRD NONDETERMINISTIC ALGORITHM - PREPARATION
ALG(t,k,n,r,R)* is a modification of ALG(t,k,n,r,R)/1. It is presented
only to aid in the understanding of the next section algorithm.
Here t >= (8knr)!! and R be an irreflexive and symmetric order
invariant relation on N^k. And as before, the algorithm takes place in
[0,nt]^k.
DEFINITION 4.1. x in N^k is primary if and only if there is a unique
coordinate of x that is greater than all other coordinates. x in N^k
is secondary if x is not primary. The lower coordinates of x in N^k
are the coordinates that are less than the max.
DEFINITION 4.2. Let x be in [0,nt]^k. ush(x;t) results from adding t
to all coordinates of x that are >= t if this stays in [0,nt]^k; x
otherwise. ush is read "upper shift".
DEFINITION 4.3. W is the set of floors of geometric means of 0,t and
t,2t and ... and (n-1)t,nt. Thus |W| = n-1.
We will be using a specific D,D', both subsets of the secondary
k-tuples whose maximum coordinate lies in W.
ALG(t,k,n,r,R)* is in r stages and produces sets A_1
containedin ... containedin A_r containedin [0,nt]^k, and sets
B_1,...,B_r containedin [0,nt]^k.
We initialize by setting A_1 = emptyset. B_1 = ({0,t,2t,...,nt} union W)^k.
Suppose A_i and B_i have been constructed.
case 1. B_i = emptyset. Set A_i+1 = A_i and "refresh" B. I.e., B_i+1 =
fld(A_i)^k.
case 2. B_i not= emptyset. We "process" some element of B_i. I.e.,
choose any u in B_i. Set B_i+1 = B_i\{u}.
case 2a. If u is primary then choose any x in N^k not R related to u,
with max(x) <= max(u), and set A_i+1 = A_i union {x,ush(x;t)}.
case 2b. If u is secondary then set A_i+1 = A_i union {u} or A_i+1 = A_i.
This execution of ALG(t,k,n,r,R)* is considered SUCCESSFUL if and
only if any two elements of A_r are R related.
BIG OPENING: Put conditions down about how case 2b is executed.
The default execution of case 2b is to always set A_i+1 = A_i.
PROPOSITION 4.1. ALG(t,k,n,r,R)* can be successfully executed under
the default execution of case 2b.
THEOREM 4.2. Proposition 4.1 is provably equivalent to Con(SRP) over EFA.
5. THIRD NONDETERMINISTIC ALGORITHM - Pi01 incompleteness Con(HUGE
Let t,k,n,r,R be as in section 4 and let D contained in [0,nt]^k.
ALG(t,k,n,r,R,D)/3 is the same as ALG(t,k,n,r,R)* but where case 2b is
executed as follows:
case 2b. If u is secondary then set A_i+1 = A_i union {u} if u in D;
A_i+1 = A_i otherwise.
We take D = {x in [0,nt]^k: x is secondary, max(x) in W, and there are
exactly two lesser coordinates of x, one the other plus t.
PROPOSITION 5.1. ALG(t,k,n,r,R,D)/3 can be successfully executed.
THEOREM 5.2. Proposition 4.1 is provably equivalent to Con(HUGE) over EFA.
As in section 3, we can use the method of declining refreshes to
create ALG(t,k,n,R,D) whose successful executions are equivalent to
1-Con(HUGE), and with fast growing functions.
Also we can create a template leveraging off of the great simplicity
of the set D we use here.
##########################################
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 894th 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
800: Beyond Perfectly Natural/6 4/3/18 8:37PM
801: Big Foundational Issues/1 4/4/18 12:15AM
802: Systematic f.o.m./1 4/4/18 1:06AM
803: Perfectly Natural/7 4/11/18 1:02AM
804: Beyond Perfectly Natural/8 4/12/18 11:23PM
805: Beyond Perfectly Natural/9 4/20/18 10:47PM
806: Beyond Perfectly Natural/10 4/22/18 9:06PM
807: Beyond Perfectly Natural/11 4/29/18 9:19PM
808: Big Foundational Issues/2 5/1/18 12:24AM
809: Goedel's Second Reworked/1 5/20/18 3:47PM
810: Goedel's Second Reworked/2 5/23/18 10:59AM
811: Big Foundational Issues/3 5/23/18 10:06PM
812: Goedel's Second Reworked/3 5/24/18 9:57AM
813: Beyond Perfectly Natural/12 05/29/18 6:22AM
814: Beyond Perfectly Natural/13 6/3/18 2:05PM
815: Beyond Perfectly Natural/14 6/5/18 9:41PM
816: Beyond Perfectly Natural/15 6/8/18 1:20AM
817: Beyond Perfectly Natural/16 Jun 13 01:08:40
818: Beyond Perfectly Natural/17 6/13/18 4:16PM
819: Sugared ZFC Formalization/1 6/13/18 6:42PM
820: Sugared ZFC Formalization/2 6/14/18 6:45PM
821: Beyond Perfectly Natural/18 6/17/18 1:11AM
822: Tangible Incompleteness/1 7/14/18 10:56PM
823: Tangible Incompleteness/2 7/17/18 10:54PM
824: Tangible Incompleteness/3 7/18/18 11:13PM
825: Tangible Incompleteness/4 7/20/18 12:37AM
826: Tangible Incompleteness/5 7/26/18 11:37PM
827: Tangible Incompleteness Restarted/1 9/23/19 11:19PM
828: Tangible Incompleteness Restarted/2 9/23/19 11:19PM
829: Tangible Incompleteness Restarted/3 9/23/19 11:20PM
830: Tangible Incompleteness Restarted/4 9/26/19 1:17 PM
831: Tangible Incompleteness Restarted/5 9/29/19 2:54AM
832: Tangible Incompleteness Restarted/6 10/2/19 1:15PM
833: Tangible Incompleteness Restarted/7 10/5/19 2:34PM
834: Tangible Incompleteness Restarted/8 10/10/19 5:02PM
835: Tangible Incompleteness Restarted/9 10/13/19 4:50AM
836: Tangible Incompleteness Restarted/10 10/14/19 12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20 02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory 2/8/20 2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20 12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1: 5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1 5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1 6/19/20 1132PM :
860: Unary Regressive Growth/1 8/120 9:50PM
861: Simplified Axioms for Class Theory 9/16/20 9:17PM
862: Symmetric Semigroups 2/2/21 9:11 PM
863: Structural Mapping Theory/1 2/4/21 11:36PM
864: Structural Mapping Theory/2 2/7/21 1:07AM
865: Structural Mapping Theory/3 2/10/21 11:57PM
866: Structural Mapping Theory/4 2/13/21 12:47AM
867: Structural Mapping Theory/5 2/14/21 11:27PM
868: Structural Mapping Theory/6 2/15/21 9:45PM
869: Structural Proof Theory/1 2/24/21 12:10AM
870: Structural Proof Theory/2 2/28/21 1:18AM
871: Structural Proof Theory/3 2/28/21 9:27PM
872: Structural Proof Theory/4 2/28/21 10:38PM
873: Structural Proof Theory/5 3/1/21 12:58PM
874: Structural Proof Theory/6 3/1/21 6:52PM
875: Structural Proof Theory/7 3/2/21 4:07AM
876: Structural Proof Theory/8 3/2/21 7:27AM
877: Structural Proof Theory/9 3/3/21 7:46PM
878: Structural Proof Theory/10 3/3/21 8:53PM
879: Structural Proof Theory/11 3/4/21 4:22AM
880: Tangible Updates/1 4/15/21 1:46AM
881: Some Logical Thresholds 4/29/21 11:49PM
882: Logical Strength Comparability 5/8/21 5:49PM
883: Tangible Incompleteness Lecture Plans 5/16/21 1:29:44
884: Low Strength Zoo/1 5/16/21 1:34:
885: Effective Forms 5/16/21 1:47AM
886: Concerning Natural/1 5/16/21 2:00AM
887: Updated Adventures 9/9/21 9:47AM 2021
888: New(?) kinds of questions 9/9/21 12:32PM
889: Generating r.e. sets 9/12/21 3:38PM
890: Update on Tangible Incompleteness 9/18/21 9:50AM :
891: Remarks on Reverse Mathematics/1 9/21/21 12:50AM :
892: Remarks on Reverse Mathematics/2 9/21/21 8:37AM :
893: Remarks on Reverse Mathematics/3 9/23/21 10:04PM
Harvey Friedman
More information about the FOM
mailing list