[FOM] 496:Invariant Finite Choice/restatement

Harvey Friedman friedman at math.ohio-state.edu
Sun Apr 8 02:18:21 EDT 2012

THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION

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

THIS POSTING IS COMPLETELY SELF CONTAINED

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

There were some small inaccuracies and unnecessary definitions in http://www.cs.nyu.edu/pipermail/fom/2012-April/016417.html
We restate everything.

INVARIANT FINITE DETACHED CHOICE
by
Harvey M. Friedman
April 8, 2012

1. Finite Detached Choice.
2. Upper A Invariance.
3. Invariant Finite Detached Choice.

1. FINITE DETACHED CHOICE.

A binary relation R on {1,...,n}^k is regressive if and only if for
all x,y in {1,...,n}^k, R(x,y) implies max(x) > max(y) or x = y.

We say that a function is detached (with respect to R) if and only if
no two distinct values are related by R.

We identify functions with their graphs.

FINITE DETACHED CHOICE. Every reflexive regressive relation on
{1,...,n}^k contains a detached f:{1,...,n}^k into {1,...,n}^k. Any
two such f have the same fixed points.

We can view such an f as a detached choice function for the relation.

The finite length inductive proof is pleasantly elementary and
educational.

2. UPPER A INVARIANCE.

Let A be a nonempty finite set of positive integers. We say that x,y
in are upper A equivalent if and only if

i. x,y in {1,...,max(A)}}^k
ii. x,y are each strictly increasing.
iii. All coordinates not in the longest common initial subsequence of
x,y lie in A.

We say that S is upper A invariant if and only if for all upper A
equivalent x,y, if x in S then y in S.

3. INVARIANT FINITE DETACHED CHOICE THEOREM.

We write f::U into V into W into X if and only if f maps all of U into
V, all of V into W, and all of W into X.

INVARIANT FINITE DETACHED CHOICE. Every reflexive regressive relation
on {1,...,n}^k contains a detached f::A^k into B^k into C^k into D^k, |
A| >= log*(n)/(8k)!, with upper A invariant range.

We can view a detached function contained in a relation as a partial
detached choice function for that relation.

Here log*(n) is the number of times log can be applied to n. The (8k)!
is overkill. We'll see what we really need in due course.

THEOREM. Invariant Finite Detached Choice is equivalent to Con(SRP)
over ACA'.

SRP = ZFC + {there exists lambda with the k-SRP}_k. Lambda has the k-
SRP iff lambda is a limit ordinal, where every partition of the
unordered k-tuples from lambda into two pieces has a stationary
homogeneous set. ACA' = RCA_0 + for all x,n, the n-th Turing jump of x
exists.

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

manuscripts. This is the 496th 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-449 can be found
in the FOM archives at http://www.cs.nyu.edu/pipermail/fom/2010-December/015186.html

450: Maximal Sets and Large Cardinals II  12/6/10  12:48PM
451: Rational Graphs and Large Cardinals I  12/18/10  10:56PM
452: Rational Graphs and Large Cardinals II  1/9/11  1:36AM
453: Rational Graphs and Large Cardinals III  1/20/11  2:33AM
454: Three Milestones in Incompleteness  2/7/11  12:05AM
455: The Quantifier "most"  2/22/11  4:47PM
456: The Quantifiers "majority/minority"  2/23/11  9:51AM
457: Maximal Cliques and Large Cardinals  5/3/11  3:40AM
458: Sequential Constructions for Large Cardinals  5/5/11  10:37AM
459: Greedy CLique Constructions in the Integers  5/8/11  1:18PM
460: Greedy Clique Constructions Simplified  5/8/11  7:39PM
461: Reflections on Vienna Meeting  5/12/11  10:41AM
462: Improvements/Pi01 Independence  5/14/11  11:53AM
463: Pi01 independence/comprehensive  5/21/11  11:31PM
464: Order Invariant Split Theorem  5/30/11  11:43AM
465: Patterns in Order Invariant Graphs  6/4/11  5:51PM
467: Comment on Minimal Dominators  6/14/11  11:58AM
468: Maximal Cliques/Incompleteness  7/26/11  4:11PM
469: Invariant Maximality/Incompleteness  11/13/11  11:47AM
470: Invariant Maximal Square Theorem  11/17/11  6:58PM
471: Shift Invariant Maximal Squares/Incompleteness  11/23/11  11:37PM
472. Shift Invariant Maximal Squares/Incompleteness  11/29/11  9:15PM
473: Invariant Maximal Powers/Incompleteness 1  12/7/11  5:13AMs
474: Invariant Maximal Squares  01/12/12  9:46AM
475: Invariant Functions and Incompleteness  1/16/12  5:57PM
476: Maximality, CHoice, and Incompleteness  1/23/12  11:52AM
477: TYPO  1/23/12  4:36PM
478: Maximality, Choice, and Incompleteness  2/2/12  5:45AM
479: Explicitly Pi01 Incompleteness  2/12/12  9:16AM
480: Order Equivalence and Incompleteness
481: Complementation and Incompleteness  2/15/12  8:40AM
482: Maximality, Choice, and Incompleteness 2  2/19/12 7:43AM
483: Invariance in Q[0,n]^k  2/19/12  7:34AM
484: Finite Choice and Incompleteness  2/20/12  6:37AM__
485: Large Large Cardinals  2/26/12  5:55AM
486: Naturalness Issues  3/14/12  2:07PM
487: Invariant Maximality/Naturalness  3/21/12  1:43AM
488: Invariant Maximality Program  3/24/12  12:28AM
489: Invariant Maximality Programs  3/24/12  2:31PM
490: Invariant Maximality Program 2  3/24/12  3:19PM
491: Formal Simplicity  3/25/12  11:50PM
492: Invariant Maximality/conjectures  3/31/12  7:31PM
493: Invariant Maximality/conjectures 2  3/31/12  7:32PM
494: Inv Max Templates/Z+up, upper Z+ equiv  4/5/12  4:17PM
495: Invariant Finite Choice  4/5/12  4:18PM

Harvey Friedman