[FOM] 798: Beyond Perfectly Natural/4
Harvey Friedman
hmflogic at gmail.com
Sat Mar 31 17:30:24 EDT 2018
THIS POStTNG IS SELF CONTAINED
this can be understood without knowing the cited formal systems
EFA = exponential function arithmetic
RCA_0 is my base theory for my Reverse Mathematics
ACA' is "for all n,x, the n-th jump of x exists"
SMAH is the scheme of strongly k-Mahlo cardinals
I now present a new finite form in Inductive Equation Theory. I was
playing around with ideas like this before but it has only jelled now.
1. INFINITE COMPLEMENTATION
2. FINITE COMPLEMENTATION
3. REMARKS
1. INFINITE COMPLEMENTATION
DEFINITION 1.1. N is the set of all nonnegative integers. Let R
containedin N^k x N^k. We view R as a binary relation on N^k. R[A] =
{y: (there exists x in A)(x R y)}. R<[A} = {y: (there exists x in A)(x
R y and max(x) < max(y)}. The appearance of R[A] or R<[A] implies that
A containedin N^k.
COMPLEMENTATION. For R containedin N^k x N^k, some A U. R<[A] is N^k.
Furthermore, A is unique.
This Complementation Theorem captures a particularly transparent form
of recursion along the positive integers in a very fundamental way.
We are particularly interested in very explicit R containedin N^k x N^k.
DEFINITION 1.2. x,y in N^k are order equivalent if and only if for all
1 <= i,j <= k, x_i < x_j iff y_i < y_j. S containedin N^k is order
invariant if and only if for all order equivalent x,y in N^k, S(x) iff
S(y). R containedin N^k x N^k is order invariant if and only if R is
order invariant as a subset of N^2k.
EXPLICIT COMPLEMENTATION. EC. For order invariant R containedin N^k x
N^k, some A U. R<[A] is N^k Furthermore, A is unique and of low
interesting computational complexity. These results are provable in
RCA_0.
Note that there are only roughly a double exponential number of sets A
containedin N^k arising from EC.
DEFINITION 1.3. Let A containedin N^k. The order invariant images of A
are the R[A] for order invariant R containedin N^k x N^k. The n/exp
order invariant images of A^k in N^k are the R[A^k], where R
containedin (N^k)^k x N^k is order invariant with parameters from
1,n,n^2,...
EXPLICIT COMPLEMENTATION/EXP. EC/EXP. For order invariant R
containedin N^k x N^k, some A U. R<[A] has a tuple in common with
every nonempty n/exp order invariant image of A (the tuple depending
on the image).
So far, EIC and CIC are obvious special cases of IC.
EXOTIC COMPLEMENTATION. EXC. For n > (8k)!! and order invariant R
containedin N^k x N^k, some A U. R<[A] has a tuple without n-1, in
common with every nonempty n/exp order invariant image of A^k in N^k
(the tuple depending on the image).
Here (8k)!! is safe convenient overkill.
EXC is independent of ZFC. We can in fact prove that A can be found to
be not only of low computational complexity, but with a rather
explicit representation.
THEOREM 1.1. EXC is provably equivalent, over ACA', to Con(SMAH). This
holds even if we replace A^k by A^2.
The statement of EXC stated with low computational complexity puts it
in explicitly Pi03 form. The rather explicit representation and well
known decision procedures puts it in explicitly Pi01 form. The
explicit representations will be taken up in later postings.
However, the finite forms in section 2 are completely straightforward
and do not add any significant complications - and they are explicitly
Pi01.
2. FINITE COMPLEMENTATION
DEFINITION 2.1. [t] = {0,...,t|. Let R containedin [t]^k x [t]^k. We
view R as a binary relation on [t]^k. R[A] = {y: (there exists x in
A)(x R y)}. R<[A} = {y: (there exists x in A)(x R y and max(x) <
max(y)}. The appearance of R[A] or R<[A] implies that A containedin
[t]^k.
FINITE COMPLEMENTATION. For R containedin [t]^k x [t]^k, some A U.
R<[A] is [t]^k. Furthermore, A is unique.
This Complementation Theorem captures a particularly transparent form
of finite recursion in a very fundamental way.
We are particularly interested in very explicit R containedin [t]^k x [t]^k.
DEFINITION 2.2. S containedin [t]^k is order invariant if and only if
for all order equivalent x,y in [t]^k, S(x) iff S(y). R containedin
[t]^k x [t]^k is order invariant if and only if R is order invariant
as a subset of [t]^2k.
DEFINITION 2.3. Let A containedin [t]^k. The order invariant images of
A are the R[A] for order invariant R containedin [t]^k x [t]^k. The
n/exp order invariant images of A in [t]^k are the R[A^k], where R
containedin ([t]^k)^k x [t]^k is order invariant with parameters from
the 1,n,n^2,... in [t].
FINITE EXOTIC COMPLEMENTATION. FEXC. For (8k)! < n < t and order
invariant R containedin [t]^k x [t]^k, some A U. R<[A] has a tuple
without n-1, in common with every nonempty n/exp order invariant image
of A^k in [t]^k (the tuple depending on the image).
Here (8k)!! is safe convenient overkill.
FEXC is independent of ZFC.
THEOREM 2.1. FEXC is provably equivalent, over ACA', to Con(SMAH).
This holds even if we replace A^k by A^2.
The statement of FEXC is obviously Pi01.
3. REMARKS
FEXC appears to be our most convincing explicitly Pi01 sentence
independent of ZFC at this time. For some readers FEXC will be the
their favorite over all of my concrete incompleteness from ZFC,
including the implicitly Pi01 sentences.
HOWEVER, FEXC does not have the feel - at least not at this time - of
being the start of a major long term thematically enticing
investigation that requires large cardinals for the main results.
There is, however, some prospect for building some theory surrounding
the templating of Complementation.
But the implicitly Pi01 sentences, especially through Emulation
Theory, seem to be - at the moment - stronger in terms of long term
thematically enticing investigations.
************************************************************************
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 798th 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-699 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
700: Large Cardinals and Continuations/14 8/1/16 11:01AM
701: Extending Functions/1 8/10/16 10:02AM
702: Large Cardinals and Continuations/15 8/22/16 9:22PM
703: Large Cardinals and Continuations/16 8/26/16 12:03AM
704: Large Cardinals and Continuations/17 8/31/16 12:55AM
705: Large Cardinals and Continuations/18 8/31/16 11:47PM
706: Second Incompleteness/1 7/5/16 2:03AM
707: Second Incompleteness/2 9/8/16 3:37PM
708: Second Incompleteness/3 9/11/16 10:33PM
709: Large Cardinals and Continuations/19 9/13/16 4:17AM
710: Large Cardinals and Continuations/20 9/14/16 1:27AM
711: Large Cardinals and Continuations/21 9/18/16 10:42AM
712: PA Incompleteness/1 9/23/16 1:20AM
713: Foundations of Geometry/1 9/24/16 2:09PM
714: Foundations of Geometry/2 9/25/16 10:26PM
715: Foundations of Geometry/3 9/27/16 1:08AM
716: Foundations of Geometry/4 9/27/16 10:25PM
717: Foundations of Geometry/5 9/30/16 12:16AM
718: Foundations of Geometry/6 101/16 12:19PM
719: Large Cardinals and Emulations/22
720: Foundations of Geometry/7 10/2/16 1:59PM
721: Large Cardinals and Emulations//23 10/4/16 2:35AM
722: Large Cardinals and Emulations/24 10/616 1:59AM
723: Philosophical Geometry/8 10/816 1:47AM
724: Philosophical Geometry/9 10/10/16 9:36AM
725: Philosophical Geometry/10 10/14/16 10:16PM
726: Philosophical Geometry/11 Oct 17 16:04:26 EDT 2016
727: Large Cardinals and Emulations/25 10/20/16 1:37PM
728: Philosophical Geometry/12 10/24/16 3:35PM
729: Consistency of Mathematics/1 10/25/16 1:25PM
730: Consistency of Mathematics/2 11/17/16 9:50PM
731: Large Cardinals and Emulations/26 11/21/16 5:40PM
732: Large Cardinals and Emulations/27 11/28/16 1:31AM
733: Large Cardinals and Emulations/28 12/6/16 1AM
734: Large Cardinals and Emulations/29 12/8/16 2:53PM
735: Philosophical Geometry/13 12/19/16 4:24PM
736: Philosophical Geometry/14 12/20/16 12:43PM
737: Philosophical Geometry/15 12/22/16 3:24PM
738: Philosophical Geometry/16 12/27/16 6:54PM
739: Philosophical Geometry/17 1/2/17 11:50PM
740: Philosophy of Incompleteness/2 1/7/16 8:33AM
741: Philosophy of Incompleteness/3 1/7/16 1:18PM
742: Philosophy of Incompleteness/4 1/8/16 3:45AM
743: Philosophy of Incompleteness/5 1/9/16 2:32PM
744: Philosophy of Incompleteness/6 1/10/16 1/10/16 12:15AM
745: Philosophy of Incompleteness/7 1/11/16 12:40AM
746: Philosophy of Incompleteness/8 1/12/17 3:54PM
747: PA Incompleteness/2 2/3/17 12:07PM
748: Large Cardinals and Emulations/30 2/15/17 2:19AM
749: Large Cardinals and Emulations/31 2/15/17 2:19AM
750: Large Cardinals and Emulations/32 2/15/17 2:20AM
751: Large Cardinals and Emulations/33 2/17/17 12:52AM
752: Emulation Theory for Pure Math/1 3/14/17 12:57AM
753: Emulation Theory for Math Logic 3/10/17 2:17AM
754: Large Cardinals and Emulations/34 3/12/17 12:34AM
755: Large Cardinals and Emulations/35 3/12/17 12:33AM
756: Large Cardinals and Emulations/36 3/24/17 8:03AM
757: Large Cardinals and Emulations/37 3/27/17 2:39AM
758: Large Cardinals and Emulations/38 4/10/17 1:11AM
759: Large Cardinals and Emulations/39 4/10/17 1:11AM
760: Large Cardinals and Emulations/40 4/13/17 11:53PM
761: Large Cardinals and Emulations/41 4/15/17 4:54PM
762: Baby Emulation Theory/Expositional 4/17/17 1:23AM
763: Large Cardinals and Emulations/42 5/817 2:18AM
764: Large Cardinals and Emulations/43 5/11/17 12:26AM
765: Large Cardinals and Emulations/44 5/14/17 6:03PM
766: Large Cardinals and Emulations/45 7/2/17 1:22PM
767: Impossible Counting 1 9/2/17 8:28AM
768: Theory Completions 9/4/17 9:13PM
769: Complexity of Integers 1 9/7/17 12:30AM
770: Algorithmic Unsolvability 1 10/13/17 1:55PM
771: Algorithmic Unsolvability 2 10/18/17 10/15/17 10:14PM
772: Algorithmic Unsolvability 3 Oct 19 02:41:32 EDT 2017
773: Goedel's Second: Proofs/1 Dec 18 20:31:25 EST 2017
774: Goedel's Second: Proofs/2 Dec 18 20:36:04 EST 2017
775: Goedel's Second: Proofs/3 Dec 19 00:48:45 EST 2017
776: Logically Natural Examples 1 12/21 01:00:40 EST 2017
777: Goedel's Second: Proofs/4 12/28/17 8:02PM
778: Goedel's Second: Proofs/5 12/30/17 2:40AM
779: End of Year Claims 12/31/17 8:03PM
780: One Dimensional Incompleteness/1 1/4/18 1:14AM
781: One Dimensional Incompleteness/2 1/6/18 11:25PM
782: Revolutionary Possibilities/1 1/12/18 11:26AM
783: Revolutionary Possibilities/2 1/20/18 9:43PM
784: Revolutionary Possibilities/3 1/21/18 2:59PM
785: Revolutionary Possibilities/4 1/22/18 12:38AM
786: Revolutionary Possibilities/5 1/24/18 12:15AM
787: Revolutionary Possibilities/6 1/25/18 4:09AM
788: Revolutionary Possibilities/7 2/1/18 2:18AM
789: Revolutionary Possibilities/8 2/1/18 9:02AM
790: Revolutionary Possibilities/9 2/2/18 3:07AM
791: Emulation Theory/Inductive Equations/1 2/8/18 11:52PM
792: Emulation Theory/Inductive Equations/2 2/25/18 12:58PM
793: Emulation Theory/Inductive Equations/3 2/27/18 12:11AM
794: Emulation Theory/Inductive Equations/4 3/6/18 9:22PM
795: Beyond Perfectly Natural/1 3/19/18 7:19PM
796: Beyond Perfectly Natural/2 3/24/18 11:29PM
797: Beyond Perfectly Natural/3 3/27/18 12:37AM
Harvey Friedman
More information about the FOM
mailing list