FOM: 146:Large large cardinals

[Harvey Friedman]

We present a Proposition trapped between the consistency of two large large
cardinal axioms, in terms of linearly ordered products, definable
relations, and nontrivial self embeddings. It is obvious that the
Proposition asserts the (countable) satisfiability of an effective set of
sentences in first order predicate calculus with equality, and so is
provably equivalent to a Pi-0-1 sentence over WKL_0.

This example is not in explicitly finite terms as in posting 145, and does
not have the blatantly elementary character of posting 126.

Instead, it is of an elementary model theoretic flavor.

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

A linearly ordered product is a triple (A,<,dot), where (A,<) is a linear
ordering and dot:A x A into A.

A definable relation is an R containedin A^k which is definable in
(A,<,dot) with parameters allowed from A.

Let R containedin A^k. We write fld(R) for the set of all coordinates of
elements of R. We say that R is unbounded if and only if for all x in A,
there exists y in fld(R) such that x <= y.

An initial restriction of R is a pair R_x = ((-infinity,x),R|(-infinity,x)).

A nontrivial self embedding of R_x is a function f:(-infinity,x) into
(-infinity,x) such that

i) f maps fld(R_x) one-one into fld(R_x);
ii) there exists y in fld(R_x) such that f(y) not= y;
iii) for all y in (-infinity,x)\fld(R_x), f(y) = min(A);
iv) for all y1,...,yk < x, R(y1,...,yk) implies R(f(y1),...,f(yk)).

We say that R_x is self embeddable if and only if it has a nontrivial self
embedding.

We say that R_x is cross sectionally self embeddable if and only if R_x has
a nontrivial self embedding f that is given by a cross section; i.e., where
for some y in A, f(z) = y dot z.

PROPOSITION 1. There is a countable linearly ordered product in which every
unbounded definable relation has a shortest cross sectionally self
embeddable initial restriction.

THEOREM 2. Proposition 1 proves the consistency of ZFC + "there are
arbitrarily large ordinals lambda such that there is a proper elementary
embedding from V(lambda) into V(lambda)" over EFA. Proposition 1 can be
proved in EFA + Con(ZFC + there is a nontrivial elementary embedding from V
into M with V(lambda) containedin M).

Furthermore, the same results hold even if we replace "relation" by "binary
relation".

SO WHAT IS NOT OBSOLETE AMONG RECENT POSTINGS? Postings 126, 145, 146.

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

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.

This is the 146th in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones counting from #100 are:

100:Boolean Relation Theory IV corrected  3/21/01  11:29AM
101:Turing Degrees/1  4/2/01  3:32AM
102: Turing Degrees/2  4/8/01  5:20PM
103:Hilbert's Program for Consistency Proofs/1 4/11/01  11:10AM
104:Turing Degrees/3   4/12/01  3:19PM
105:Turing Degrees/4   4/26/01  7:44PM
106.Degenerative Cloning  5/4/01  10:57AM
107:Automated Proof Checking  5/25/01  4:32AM
108:Finite Boolean Relation Theory   9/18/01  12:20PM
109:Natural Nonrecursive Sets  9/26/01  4:41PM
110:Communicating Minds I  12/19/01  1:27PM
111:Communicating Minds II  12/22/01  8:28AM
112:Communicating MInds III   12/23/01  8:11PM
113:Coloring Integers  12/31/01  12:42PM
114:Borel Functions on HC  1/1/02  1:38PM
115:Aspects of Coloring Integers  1/3/02  10:02PM
116:Communicating Minds IV  1/4/02  2:02AM
117:Discrepancy Theory   1/6/02  12:53AM
118:Discrepancy Theory/2   1/20/02  1:31PM
119:Discrepancy Theory/3  1/22.02  5:27PM
120:Discrepancy Theory/4  1/26/02  1:33PM
121:Discrepancy Theory/4-revised  1/31/02  11:34AM
122:Communicating Minds IV-revised  1/31/02  2:48PM
123:Divisibility  2/2/02  10:57PM
124:Disjoint Unions  2/18/02  7:51AM
125:Disjoint Unions/First Classifications  3/1/02  6:19AM
126:Correction  3/9/02  2:10AM
127:Combinatorial conditions/BRT  3/11/02  3:34AM
128:Finite BRT/Collapsing Triples  3/11/02  3:34AM
129:Finite BRT/Improvements  3/20/02  12:48AM
130:Finite BRT/More  3/21/02  4:32AM
131:Finite BRT/More/Correction  3/21/02  5:39PM
132: Finite BRT/cleaner  3/25/02  12:08AM
133:BRT/polynomials/affine maps  3/25/02  12:08AM
134:BRT/summation/polynomials  3/26/02  7:26PM
135:BRT/A Delta fA/A U. fA  3/27/02  5:45PM
136:BRT/A Delta fA/A U. fA/nicer  3/28/02  1:47AM
137:BRT/A Delta fA/A U. fA/beautification  3/28/02  4:30PM
138:BRT/A Delta fA/A U. fA/more beautification  3/28/02  5:35PM
139:BRT/A Delta fA/A U. fA/better  3/28/02  10:07PM
140:BRT/A Delta fA/A U. fA/yet better  3/29/02  10:12PM
141:BRT/A Delta fA/A U. fA/grammatical improvement  3/29/02  10:43PM
142:BRT/A Delta fA/A U. fA/progress  3/30/02  8:47PM
143:BRT/A Delta fA/A U. fA/major overhaul  5/2/02  2:22PM
144: BRT/A Delta fA/A U. fA/finesse  4/3/02  4:29AM
145:BRT/A U. B U. TB/simplification/new chapter  4/4/02  4:01AM