[FOM] 308:Large large cardinals

Harvey Friedman friedman at math.ohio-state.edu
Thu Jul 5 05:01:45 EDT 2007

We present a new statement whose strength is between the existence of a
nontrivial elementary embedding of some V(lambda) into V(lambda), and the
existence of a nontrivial elementary embedding j:V into M, where V(lambda)
containedin M. 

A partial linearly ordered product is a triple (A,<,dot), where (A,<) is a
linear ordering and dot is a partial function from A^2 into A.

A subset of A is bounded if and only if there exists x in A which is >= all
elements of A. A subset of A is unbounded if and only if it is not bounded.

Let B be a set of tuples from A. We write fld(B) for the set of all
coordinates of elements of B. We say that B is bounded (unbounded) if and
only if fld(B) is bounded (unbounded).

Let f:A^2 into A be partial. We treat f as a subset of A^3.

An initial self embedding of f is a partial function g:A into A such that

i. dom(g) is a bounded subset of fld(f) which is downward closed.
ii. rng(g) containedin dom(g).
iii. g is strictly increasing.
iv. For all x,y,z in A, f(x,y) = z iff f(gx,gy) = gz.

We say that partial h:A into A is cross sectional if and only if there
exists x in A such that for all y,z in A,

h(y) = z iff f(x,y) = z.

PROPOSITION A. There exists a partial linearly ordered product in which
every unbounded definable partial binary function has a cross sectional
initial self embedding with a least fixed point and a least non fixed point.

It is obvious by the completeness theorem for first order predicate calculus
with equality that Proposition A is provably equivalent to a Pi01 sentence,
over WKL_0.


manuscripts. This is the 308th in a series of self contained numbered
previous numbered postings #1-249 can be found at
the original.

251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
255. Controlling Pi01  11/12  5:10PM
259. Pi01 pointer  11/30/05  10:36AM
277: Strict Predicativity  4/5/06  1:58PM
282: Adventures in Pi01 Independence  5/7/06
284: Godel's Second  5/9/06  10:02AM
296: Order Calculus  7/7/06  12:13PM
302: PA Completeness  10/29/06  2:38AM
303: PA Completeness (restatement)  10/30/06  11:53AM
304: PA Completeness/strategy 11/4/06  10:57AM
305: Proofs of Godel's Second  12/21/06  11:31AM
306: Godel's Second/more  12/23/06  7:39PM
307: Formalized Consistency Problem Solved  1/14/07  6:24PM

Harvey Friedman

More information about the FOM mailing list