[FOM] 734: Large Cardinals and Emulations/29

Thu Dec 8 15:53:20 EST 2016

This is a correction to section 3 of
http://www.cs.nyu.edu/pipermail/fom/2016-December/020177.html

Section 3 concerns the finite forms. We need to fix the definition of
"finitely maximal emulation" there. The basic idea is fine. In fact we
will greatly improve on what we had in mind.

EMULATION THEORY
OUTLINE

1. INTRODUCTION.
2. INFINITE EMULATION.
   2.1.  MAXIMAL EMULATION IN Q[0,1]^k.
http://www.cs.nyu.edu/pipermail/fom/2016-October/020107.html
      2.1.1. TRANSLATION.
http://www.cs.nyu.edu/pipermail/fom/2016-October/020107.html
      2.1.2. EMBEDDING.
http://www.cs.nyu.edu/pipermail/fom/2016-October/020137.html
   2.2. STEP MAXIMAL EMULATION IN Q^k.
http://www.cs.nyu.edu/pipermail/fom/2016-November/020170.html
   2.3. GREEDY EMULATION IN Q^k.
http://www.cs.nyu.edu/pipermail/fom/2016-December/020177.html
   2.4. UP GREEDY EMULATION IN Q^k.
http://www.cs.nyu.edu/pipermail/fom/2016-December/020177.html
3. FINITE EMULATION.
here

3. FINITE EMULATION

Here we use an essentially uniform method of converting all of the
main statements in section 2 to explicitly Pi02 statements. These are
then easily converted to explicitly Pi01 statements using obvious
upper bounds.

Recall the definition of order invariant subsets of the Q^k. Of the
several equivalent definitions, we can them to be the order theoretic
subsets of the Q^k without parameters.

DEFINITION 3.1. Let E,S containedin Q^k be finite, Every order
invariant F:Q^(2k^2) into Q^k gives rise to the lexicographically
least value of F over the subdomain (E x S)^k. The E,S minimal tuples
are k-tuples that so arise.

DEFINITION 3.2. S is a finitely maximal r-emulation of finite E
containedin Q[0,1]^k if and only if S is a finite r-emulation of E
where no S U. {x} is an r-emulation of E containedin Q[0,1]^k with x
E,S minimal. We make the same definition with Q[0,1] replaced by Q.

FMED/1. For finite subsets of Q[0,1]^k, some finitely maximal
emulation (r-emulation) is drop equivalent from (1,1/2,...,1/k) to
(1/2,...,1/k,1/k).

DEFINITION 3.3. S is a finitely greedy r-emulation of finite E
containedin Q^k if and only if S is a finite r-emulation of E where no
S|<x U. {x} is an r-emulation of E containedin Q^k with x E,S minimal. S
is a finitely greedy emulation of finite E containedin Q^k if and only
if S is a finitely greedy 2-emulation of finite E containedin Q^k.

Recall the previous definition of the upper shift ush(S) of subsets S
of Q^k. ush(S) is the result of adding 1 to all nonnegative
coordinates of all elements of S.

FGES/1. Every finite subset of Q^k has a finitely greedy emulation
(r-emulation) containing its upper shift |<=k.

DEFINITION 3.4. S is a finitely up greedy r-emulation of finite E
containedin Q^k if and only if S is a finite r-emulation of E where no
S|<x U. {x} is an r-emulation of E containedin Q^ with x E,S minimal
and increasing. S is a finitely up greedy emulation of finite E
containedin Q^k if and only if S is a finitely up greedy 2-emulation
of finite E containedin Q^k.

FUGES/1. Every finite subset of Q^k has a finitely up greedy emulation
(r-emulation) containing its upper shift |<=k.

FUGES/2. Every finite subset of Q^k has a finitely up greedy emulation
(r-emulation) S where each ush(S)|<=i, i <= k, is an elementary subset
of S with parameter i+(1/2i).

FMED/1, FGES/1, FUGES/1, FUGES/2 are explicitly Pi02 and become
explicitly Pi01 by placing an upper bound. We can use this method for
converting other implicitly Pi01 statements from section 2 to
explicitly Pi01.

THEOREM 3.1. FMED/1, FGES/1, FUGES/1 are provably equivalent to
Con(SRP) over EFA. FUGES/2 is provably equivalent to Con(HUGE) over
EFA.

************************************************************************
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 734th 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/2316  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

Harvey Friedman