942: New Stable Maximality/2

Harvey Friedman hmflogic at gmail.com
Fri Jul 29 20:47:23 EDT 2022


We now discuss Finite Stable Maximality. The statements in Stable
Maximality/3 are all implicitly Pi01 as can be easily seen using
Goedle's Completeness Theorem. The Pi01 equivalents lose their
extremely basic transparent mathematical character. In finite Stable
Maximality we seek to preserve that extremely basic transparent
mathematical character while at the same time being explicitly Pi01.

GREEDY MAXIMAL EMULATOR(k,n). GRME(k,n). Input is nonempty finite E
containedin Q[-n,n]^k. and sequence x_1,x_2,... from Q[-n,n]^k of
nonzero finite or infinite length. We successively change each x_i to
x_i' (sometimes x_i' = x_i) starting with x_1 to x_1', as follows.
x_1' is x_1 if {x_1} is an emulator of E containedin Q[-n,n]^k.
Otherwise x_1' is an element of E (lexicographically least for
specificity). Suppose x_1',...,x_i' have been defined and
{x_1',...,x_i'} is an emulator of E containedin Q[-n,n]^k.

Here GRME is read "greedy maximal emulator".

THEOREM 1. GRME(k,n) can be completed (deterministically), with any
input, resulting in an emulator of E containedin Q[-n,n]^k. If the
input sequence enumerates exactly Q[-n,n]^k then the result is a
maximal emulator of E.

We now give a nondeterministic form of GME(k,n) where Theorem 1 is
preserved. We will be inserting new rationals, and so we use the
following definition for control.

DEFINITION 1. Let x_1,...,x_t in Q* and y in Q*. We say that y is
balanced over x_1,...,x_t if and only if the following holds. Let p <
q be adjacent elements of the union of N with the collective
coordinates of x_1,...,x_t. Then p followed by the coordinates of y
followed by q forms an arithmetic progression. I.e., we have equal
spacing.

NONDETERMINISTIC MAXIMAL EMULATOR(k,n). NOME(k,n). Input is nonempty
finite E containedin Q[-n,n]^k. and sequence x_1,x_2,... from
Q[-n,n]^k of nonzero finite or infinite length. We successively change
each x_i to x_i' (sometimes x_i' = x_i) starting with x_1 to x_1', as
follows. Suppose x_1',...,x_i-1' has been constructed where
{x_1',...,x_i-1'} is an emulator of E. Then x_i' is required to be
balanced over x_1,...,x_i, and {x_1',...,x_i'} is an emulator of E
containedin Q[-n,n]^k, and
i. x_i' = x_i; or
ii.  x_i' blocks x_i. I.e., {x_i,x_i'} is not an emulator of E.

THEOREM 2.  NOME(k,n) can be completed (nondeterministically), with
any input, resulting in an emulator of E containedin Q[-n,n]^k. Any
partial completion can be extended to a completion. If the input
sequence enumerates exactly Q[-n,n]^k then the result is a maximal
emulator of E containedin Q[-n,n]^k.

THEOREM 3. At a given input, the set of tuples resulting from apply
GME(k,n) can be obtained from applying NOME(k,n).

So what can we do with the added flexibility of this nondeterministic
form NOME(k,n) that we can't do with the deterministic greedy form
GME(k,n)?

Recall NTS:Q^k into Q^k from Stable Maximality/1.

DEFINITION 2. An execution of NOME(k,n) is stable if and only if for
all x_i, and x_j = NTS(x_i), we have x_i = x_i' iff x_j = x_j'.

FINITE STABLE MAXIMAL EMULATOR(k,n). FSME(k,n). NOME(k,n) has a stable
execution for every finite input.

FINITE STABLE MAXIMAL EMULATOR. FSME. For all k,n, NOME(k,n) has a
stable execution for every finite input.

THEOREM 4. FSME is provably equivalent to Con(SRP) over EFA.

Note that FSME is explicitly Pi01 because of the balancing from Definition 1.

##########################################

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 942nd 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-899 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1  10/13/21 10:22PM
908: Base Theory Proposals for Third Order RM/2  10/17/21 3:15PM
909: Base Theory Proposals for Third Order RM/3  10/17/21 3:25PM
910: Base Theory Proposals for Third Order RM/4  10/17/21 3:36PM
911: Ultra Convergence/3  1017/21  4:33PM
912: Base Theory Proposals for Third Order RM/5  10/18/21 7:22PM
913: Base Theory Proposals for Third Order RM/6  10/18/21 7:23PM
914: Base Theory Proposals for Third Order RM/7  10/20/21 12:39PM
915: Base Theory Proposals for Third Order RM/8  10/20/21 7:48PM
916: Tangible Incompleteness and Clique Construction/1  12/8/21   7:25PM
917: Proof Theory of Arithmetic/1  12/8/21  7:43PM
918: Tangible Incompleteness and Clique Construction/1  12/11/21  10:15PM
919: Proof Theory of Arithmetic/2  12/11/21  10:17PM
920: Polynomials and PA  1/7/22  4:35PM
921: Polynomials and PA/2  1/9/22  6:57 PM
922: WQO Games  1/10/22 5:32AM
923: Polynomials and PA/3  1/11/22  10:30 PM
924: Polynomials and PA/4  1/13/22  2:02 AM
925: Polynomials and PA/5  2/1/22  9::04PM
926: Polynomials and PA/6  2/1/22 11:20AM
927: Order Invariant Games/1  03/04/22  9:11AM
928: Order Invariant Games/2  03/7/22  4:22AM
929: Physical Infinity/randomness  3/21/22 02:14AM
930: Tangible Indiscernibles/1 05/07/22  7:46PM
931: Tangible Indiscernibles/2 5/14/22  1:34PM
932: Tangible Indiscernibles/3  5/14/22  1:34PM
933: Provable Functions of Set Theories/1 5/16/22  7/11AM
934: Provable Ordinals of Set Theories/1  5/17/22  8:35AM
935: Stable Maximality/Tangible Incompleteness/1  6/3/22  7:05PM
936: Stable Maximality/Tangible Incompleteness/2  6/4/22  11:31PM
937: Logic of Real Numbers/1  6/22/22  7:49AM
938: Logic of Real Functions/1 7/9/22  2:42AM
939: Stable Maximality/1  7/22/22  10:07AM
940: Stable Maximality/2  7/24/2 19:19:48 EDT 2022
941: Stable Maximality/3

Harvey Friedman


More information about the FOM mailing list