# [FOM] 835: Tangible Incompleteness Restarted/9

Harvey Friedman hmflogic at gmail.com
Sun Oct 13 04:50:06 EDT 2019

```I have now placed this on my website:

109. Tangible Incompleteness Interim Report October 12, 2019, 19 pages.

#109 treats sections 2.1, 2.2, 2.3.

TANGIBLE INCOMPLETENESS - book

1. BOOLEAN RELATION THEORY - website

2. INVARIANT MAXIMALITY
2.1. Introduction. #109
2.2. Emulation Theory #109
2.2.1. N, Z+, Q, Q[(a,b)], Order Equivalence,
Emulator, Maximality
2.2.2. (Complete) Invariance, Shift, N Shift, N Tail, N Tail
Shift, N Tail-Related
2.2.3. Invariant Maximal Emulation
2.2.4. r-Emulation, N Order Equivalence, Uniform
Shifts, Shift Usability
2.2.5. Relation Usability
2.3. Invariant Graph Theory #109
2.3.1. (Hyper) Graphs, Order Invariant (Hyper)
Graphs, (Hyper) Cliques, Maximal (Hyper) Cliques
2.3.2. Invariant Maximal (Hyper) Cliques
2.3.3. Usability
2.4. Invariant A...A Theory - here
3. INDUCTIVE DOMAINS - in development
3.1. Inductive Domains in Q
3.2. Invariantly Inductive Domains in Q
4. SEQUENTIAL CONSTRUCTIONS - in development

************************************************************************
2.4. Invariant A...A Theory

DEFINITION 2.4.1. POW(X) is the set of all subsets of X. An A...A[<,k]
is a sentence starting with one or more universal quantifiers,
followed by a propositional combination of atomic formulas v < w and
S(v_1,...,v_k), where v,w,v_1,...,v_k are variables.

DEFINITION 2.4.2. An A...A subset of POW(Q[-n,n]^k) is a K containedin
POW(Q[-n,n]^k) of the form K = {S containedin Q[-n,n]^k: (Q[-n,n],<,S)
satisfies phi}, where phi is an A...A sentence in <,S. A point maximal
element of W containedin POW(Q[-n,n]^k is an S in W where there is no
S U. {x} in W. We also make the same definition with Q[-n,n]^k
replaced by Q^k.

IMA...A/1. Invariant Maximal A...A/1. (bad). Every nonempty A...A
subset of POW(Q[-n,n]^k) has a completely N Tail Shift invariant point maximal
element.

IMA...A/2. Invariant Maximal A...A/2. Every nonempty A...A subset of
POW(Q^k) has a completely N Tail Shift invariant point maximal element.

IMA...A/3. Invariant Maximal A...A/3. Every nonempty A...A subset of
POW(Q^k) has an N Tail-Related invariant point maximal element.

THEOREM 2.4.1.1. There is a decision procedure, demonstrably correct
in RCA_0, for determining whether an A...A subset of POW(Q[-n,n]^k) is
nonempty (depending only on k). The same holds with Q[-n,n]^k replaced
by Q^k. IMA...A/2, IMA...A/3 are implicitly Pi01 using the Goedel
Completeness Theorem.

THEOREM 2.4.1.2. IMA...A/1 is refutable in RCA_0. IMA...A/2, IMA...A3
are provable in WKL_0 + Con(SRP).

We do not know if IMA...A/2, IMA...A/3 are provable in ZFC, ACA_0, or
even RCA_0.

We can fix IMA...A/1 by restricting the A...A sentences, to good effect.

DEFINITION 2.4.3. A positive A...A subset of POW(Q[-n,n]^k) is a K
containedin POW(Q[-n,n]^k) of the form
K = {S containedin Q[-n,n]^k: (Q[-n,n],<,S) satisfies phi}, where phi
is an A...A sentence in <,S using only disjunctions and conjunctions
(no negations, implications, equivalences). We also make the same
definition with Q[-n,n]^k replaced by Q^k.

IMPA...A/1. Invariant Maximal Positive A...A/2. Every nonempty
positive A...A subset of POW(Q[-n,n]^k) has a completely N Tail Shift
invariant maximal element.

IMPA...A/2. Invariant Maximal Positive A...A/3. Every nonempty
positive A...A subset of POW(Q[-n,n]^k) has an N Tail-Related
invariant maximal element.

THEOREM 2.4.1.3. IMPA...A/1, IMPA...A/2 are implicitly Pi01 using the
Goedel Completeness Theorem. IMPA...A/1, IMPA...A/1 are provably
equivalent to Con(SRP) over WKL_0. The forward implication is provable
in RCA_0.

Note that the set of r-emulators of any finite subset of Q[-n,n]^k (or
Q^k) and the set of cliques of any order invariant r-graph on Q[-n,n]
(or Q^k) positive A...A sets. So IMPA...A/1, IMPA...A/2 immediately
imply IMMA/1, IMME/2, respectively. These in turn imply Con(SRP) and
therefore IMPA...A/1, IMPA...A/2 do.

All of the material concerning IMMA/1,2 usability, from section 2.3,
carry over without change.

#######################################
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
This is the 835th 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

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

Harvey Friedman
```