[FOM] 573: Philosophy of Incompleteness 4

Sat Jan 17 13:44:31 EST 2015

As promised in #572, Philosophy of Incompleteness 3, I posted a new
January 15, 2015 version of the extended abstract on my website:

[1]  https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
87. Perfectly Mathematically Natural Concrete Incompleteness  - order
theoretic relations. January 15, 2015, 26 pages. Extended abstract.
Supersedes January 14, 2015 version.

I have been adjusting the finite forms for SRP and HUGE. In [1], they
take the following forms.

PROPOSITION 6.1. Every order invariant R containedin Q^2k has finite
sets S_i = S_i#\R<[S_i-1] containing S_i+1 union ush(S_i+1), 1 < i <
n.

The above corresponds to SRP, and the more exotic

PROPOSITION 6.2. Every order invariant R containedin Q^2k has finite
sets S_i = S_i#\R<[S_i-1] containing S_i+1 union ush(S_i+1), and
S_i[0,n+(1/2)] = ush(S_i)[n,n], 1 < i < 2n.

corresponds to HUGE. In the usual way, these are explicitly Pi02 but
become explicitly Pi01 using a priori exponential type upper bounds.

Note that Proposition 6.1 has the general shape of a recurrence
relation with a major twist. S_i is defined from S_i-1 and itself, and
has a relationship with S_i+1. Proposition 6.2 simply adds a side
condition on the terms.

***************************************

I now want to explore the game theoretic approach to explicitly Pi01.

1. Finite Games and Incompleteness.
1.1. Order invariant Games.
1.2. Summation Games.

1. FINITE GAMES AND INCOMPLETENESS

1.1. ORDER INVARIANT GAMES

DEFINITION 1.1.1. N is the set of all nonnegative integers. Let x in
N^k. ush(t,x) is the result of adding t to all coordinates of x that
are >= t.

I describe the game G(R,k,t), where R containedin {0,...,kt}^2k.

Play consists of k alternating moves by Alice and Bob, starting with
Alice. Alice's moves are elements of {0,...,kt}^k whose coordinates
are either 0 or are coordinates of previous moves by either player.
Bob's response to Alice's x is x,ush(t,x) or some y,ush(t,y) with
max(y) < max(x) and x R y. Thus Bob's plays consist of two elements of
{0,...,kt+t}^k. Alice wins iff for some plays x,y in {0,...,kt}^k of
Bob, max(x) < max(y) and x R y.

THEOREM 1.1.1. Let R containedin {0,...,kt}^2k. Bob wins G(R,k) if we
remove the ush's from the rules.

PROPOSITION 1.1.2. Let R containedin {0,...,kt}^2k be order invariant
and t >= (8k)!. Bob wins G(R,k,t).

Obviously Proposition 1.1.2 is explicitly Pi01.

THEOREM 1.1.3. Proposition 1.1.2 is provably equivalent to Con(SRP) over RCA_0.

1.2. SUMMATION GAMES

Let V be a finite set of linear inequalities in k variables with
coefficients from {-k,...,k}. A proper V sum over S containedin N is a
sum

m_1 + m_2 + ... + m_k

where m_1,...,m_k in S obeys V.

I describe the game G(V,k,t), where k,t >= 1.

Play consists of alternating moves by Alice and Bob, with Bob starting
and ending the game. Alice plays k moves, and Bob plays k+1 moves. Bob
starts the game by playing a single element of {0,...,t!}. Alice's
moves are required to be in {0,1!,2!,...,t!}, or the sum of two
integers that have already been played by either player. Bob's
response to Alice's x must be x or the summands of some proper V sum
adding up to x. Alice wins iff some integer played by Bob is a proper
V sum of integers played by Bob. It is clear that no matter how the
players play, they can always complete their game.

THEOREM 1.2.1. Bob wins G(V,k,t) after playing the first move 0. Bob
also wins after playing the first move 1.

THEOREM 1.2.2. Bob wins G(V,k,t) after playing the first move (8k)!.

G(V,k,t,Bob/zero) is the same as G(V,k,t), except that Bob is not
allowed to use any previous moves of either player except Alice's last
move (if any). Thus Bob has zero memory.

THEOREM 1.2.3. Bob wins G(V,k,t,Bob/zero) after playing the first move
0. Bob also wins after playing the first move 1.

PROPOSITION 1.2.4. Bob wins G(V,k,t,Bob/zero) after playing the first
move (8k)!.

THEOREM 1.2.5. Proposition 1.2.4 is provably equivalent to Con(SMAH) over EFA.

Here SMAH is "strongly Mahlo cardinals of finite order".

If we require that t be a function of k, then the statement
corresponds to various fragments of SMAH.

************************************************************
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 573rd 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-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html

528: More Perfect Pi01  8/16/14  5:19AM
529: Yet more Perfect Pi01 8/18/14  5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01  8/22/14  5:16PM
532: More General Theory/Perfect Pi01  8/23/14  7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14  1:17AM
534: Perfect Explicitly Pi01  8/27/14  10:40AM
535: Updated Perfect Explicitly Pi01  8/30/14  2:39PM
536: Pi01 Progress  9/1/14 11:31AM
537: Pi01/Flat Pics/Testing  9/6/14  12:49AM
538: Progress Pi01 9/6/14  11:31PM
539: Absolute Perfect Naturalness 9/7/14  9:00PM
540: SRM/Comparability  9/8/14  12:03AM
541: Master Templates  9/9/14  12:41AM
542: Templates/LC shadow  9/10/14  12:44AM
543: New Explicitly Pi01  9/10/14  11:17PM
544: Initial Maximality/HUGE  9/12/14  8:07PM
545: Set Theoretic Consistency/SRM/SRP  9/14/14  10:06PM
546: New Pi01/solving CH  9/26/14  12:05AM
547: Conservative Growth - Triples  9/29/14  11:34PM
548: New Explicitly Pi01  10/4/14  8:45PM
549: Conservative Growth - beyond triples  10/6/14  1:31AM
550: Foundational Methodology 1/Maximality  10/17/14  5:43AM
551: Foundational Methodology 2/Maximality  10/19/14 3:06AM
552: Foundational Methodology 3/Maximality  10/21/14 9:59AM
553: Foundational Methodology 4/Maximality  10/21/14 11:57AM
554: Foundational Methodology 5/Maximality  10/26/14 3:17AM
555: Foundational Methodology 6/Maximality  10/29/14 12:32PM
556: Flat Foundations 1  10/29/14  4:07PM
557: New Pi01  10/30/14  2:05PM
558: New Pi01/more  10/31/14 10:01PM
559: Foundational Methodology 7/Maximality  11/214  10:35PM
560: New Pi01/better  11/314  7:45PM
561: New Pi01/HUGE  11/5/14  3:34PM
562: Perfectly Natural Review #1  11/19/14  7:40PM
563: Perfectly Natural Review #2  11/22/14  4:56PM
564: Perfectly Natural Review #3  11/24/14  1:19AM
565: Perfectly Natural Review #4  12/25/14  6:29PM
566: Bridge/Chess/Ultrafinitism 12/25/14  10:46AM
567: Counting Equivalence Classes  1/2/15  10:38AM
568: Counting Equivalence Classes #2  1/5/15  5:06AM
569: Finite Integer Sums and Incompleteness  1/515  8:04PM
570: Philosophy of Incompleteness 1  1/8/15 2:58AM
571: Philosophy of Incompleteness 2  1/8/15  11:30AM
572: Philosophy of Incompleteness 3  1/12/15  6:29PM

Harvey Friedman