[FOM] 0# over L

[Harvey Friedman]

First a remark about something I said in
http://www.cs.nyu.edu/pipermail/fom/2016-April/019771.html

I was asking about positive results concerning the naturalness of 0#
over L., pointing to the negative results concerning old conjectures
of Solovay, and the positive Jensen covering theorem. But I also
mentioned the very good situation with the Turing jump, and also the
hyperarithmetic hierarchy. There you can look at things like 2-least
upper bounds on the naturally lesser degrees. I inquired about the
hyperjump, since you can't get there in quite the same way. But I had
forgotten that you can get to the hyperjump by looking at ENUMERATIONS
of the earlier degrees, not just the degrees themselves.

This thinking about Jensen covering led me to the present posting.

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

Here we create a simple language with the aim of showing that every
sentence in the language is decidable in ZFC + 0# exists; and some
sentence in the language is provably equivalent to 0# exists over ZFC.

Actually, we present a fundamental structure, and consider the first
order sentences in that structure.

The structure is (V,L,inclusion,equinumerosity).  L is the unary
predicate whose extension consists of the constructible sets,
inclusion is the usual subset relation - NOT the epsilon relation!
Equinumerosity is the usual notion of "having the same cardinality"
from the point of view of V.

There should be a standard elimination of quantifiers treatment of
(V,inclusion,equinumerosity), which should give a very nice complete
recursive axiomatization. And it should be the same with V replaced by
any model of ZFC.

CONJECTURE. There is an elementary recursive set T of sentences
(finite?) such that, provably in ZFC + 0# exists, T is the theory of M
= (V,L,inclusion,equinumerosity). ZFC + 0# exists is the minimum
theory, compatible with ZFC + 03 exists, which decides the truth value
of every sentence about M.

THEOREM. Some sentence about M is provably equivalent to 0# exists over ZFC.

To see this, it suffices to show that "being countable" is expressible
in M. For then, we can write Jensen's equivalence with 0# exists in
the form

"there is an uncountable set which is included in some constructible
set, and which is not contained in any constructible set of the same
cardinality."

|x| <= |y| is expressible in M, as some subset of y is equinumerous
with x. Hence |x| < |y| is expressible in M. Finiteness is expressible
in M as "no proper subset is equinumerous". Countably infinite is
expressible in M as "not finite, and every set of lesser cardinality
is finite". Uncountability is therefore expressible in M.

Harvey Friedman