[FOM] 159:Elemental Sentential Reflection

[Harvey Friedman]

A PDF version of this abstract will be available in a few days on
http://www.mathpreprints.com/math/Preprint/show/

ELEMENTAL SENTENTIAL REFLECTION
by
Harvey M. Friedman
Ohio State University
Princeton University
friedman at math.ohio-state.edu
http://www.math.ohio-state.edu/~friedman/
http://www.mathpreprints.com
February 6, 2003
March 3, 2002

Abstract. "Sentential reflection" in the sense of [Fr03] is based on
reflecting down from a category of classes. "Elemental sentential
reflection" is based on reflecting down from a category of elemental
classes. We present various forms of elemental sentential reflection,
which are shown to interpret and be interpretable in certain set
theories with large cardinal axioms.

1. Introduction.

As in [Fr03], we use "class" as a neutral term, without commitment to
the developed notions of "set" and "class" that have become standard
in set theory and mathematical logic. We use epsilon for membership.

This framework supports interpretations of sentential reflection that
may differ from conventional set theory or class theory. However, we
do not pursue this direction here.

As in [Fr03], this framework is intended to accommodate objects that
are not classes. Such nonclasses are treated as classes with no
elements. Thus we are careful not to assume extensionality. In fact,
we will not assume any form of extensionality.

As in [Fr03], all of our formal theories of classes are in the
language L(epsilon), which is the usual classical first order predicate
calculus with only the binary relation symbol epsilon (no equality).

As in [Fr03], we use "category of classes" or just "category" as a
neutral term, not specifically related to category theory. They are
given by a formula of L(epsilon) with a distinguished free variable,
with parameters allowed.

In [Fr03], the following two forms of "sentential reflection" are considered.

if a given sentence of L(epsilon) holds in a given category
then it holds in a subclass.

if a given sentence of L(epsilon) holds in a given category
then it holds in an inclusion subclass.

These are called SR(epsilon) and SRIS(epsilon), respectively. In
[Fr03], they are shown to be mutually interpretable with Z_2 and ZFC,
respectively.

An elemental class is a class which is an element of a class. In some
common formalizations of the usual theory of classes that correspond
to NBG (the von Neumann Bernays Godel theory of classes), the
elemental classes are the sets, and the nonelemental classes are the
proper classes.

In "elemental sentential reflection", we reflect from a category of
elemental classes (i.e., a category all of whose elements are
elemental), to an elemental subclass (of the category of elemental
classes).

ESR(epsilon) and ESRIS(epsilon) are, respectively,

if a given sentence of L(epsilon) holds in a given category of
elemental classes then it holds in an elemental subclass.

if a given sentence of L(epsilon) holds in a given category of
elemental classes then it holds in an elemental inclusion subclass.

Just as in [Fr03] for SR(epsilon) and SRIS(epsilon), these are
formalized as double schemea, with one schematic letter presenting
the category, and one schematic letter presenting the sentence of
L(epsilon).

THEOREM 1.1. ESR(epsilon) is mutually interpretable with Z_2.
ESRIS(epsilon) is mutually interpretable with ZFC.

Thus by merely making the move to elemental sentential reflection, we
do not obtain anything new.

To take full advantage of elemental sentential reflection, we expand
the language L(() in a standard way to support quantification over
subclasses of the domain.

For this purpose, we use the two sorted language L^2(epsilon) with
variables over objects and variables over classes of objects, whose
atomic formulas are

x epsilon y
x epsilon A

where x,y are object variables and A is a class variable.

The object quantifiers are to range over the elements of the given
category or class (the domain), and the class quantifiers are to
range over all subclasses of the given category or class (the domain).

We emphasize that the language of all class theories considered here
will still be L(epsilon), despite the use of the "second order
language" L^2(epsilon).

ESR(epsilon*) is

if a given sentence of L^2(epsilon) holds in a given category of
elemental classes then it holds in an elemental subclass.

THEOREM 1.2. ESR(epsilon*) is mutually interpretable with ZFC +
{there exists a Pi-1-n indescribable cardinal}_n.

We now move to some extremely strong forms of elemental sentential
reflection. We define extensional equality as usual by x == y iff
(forall z)(z epsilon x iff z epsilon y).

Let K be a category or class. We say that x is an extensionally
proper subclass of K if and only if x is a subclass of K and
(therexists y epsilon K)(forall z == y)(z notepsilon x). Here x,y,z
are distinct variables.

ESR(epsilon*)# is

if a given sentence of L^2(epsilon) holds in a given category of
elemental classes not forming an elemental class, then it holds in a
nonelemental extensionally proper subclass.

THEOREM 1.3. ESR(epsilon*)# is interpretable in ZF + "there is a
nontrivial elementary embedding from some L(V(alpha+1)) into
L(V(alpha+1))" and interprets ZF + "there is a nontrivial elementary
embedding from some V(alpha+1) into V(alpha+1)".

It is well known that ZFC + "the existence of a measurable cardinal"
can be interpreted in ZF + "there is a nontrivial elementary
embedding from some V(alpha+1) into V(alpha+1)", or even just ZF +
"there is a nontrivial elementary embedding from some V(alpha) into
some transitive set". Such results are well known as far as the inner
model theory has been developed, which means, e.g., that "a proper
class of Woodin cardinals" can replace "the existence of a measurable
cardinal".

Woodin has many results concerning the relationship between large
cardinals above the reach of inner model theory with and without
choice.

E.g., Woodin has proved the consistency of ZFC + "there is a
nontrivial elementary embedding from some V(alpha+1) into V(alpha+1)"
from NBG + "there is a nontrivial elementary embedding from V into
V". Also Woodin has proved the consistency of ZFC + "there is a
cardinal which is n-huge for all finite n" in ZF + "there is a
nontrivial elementary embedding from some V(alpha+1) into V(alpha+1)".

Hence by Theorem 1.3 and results of Woodin, we see that ZFC + "there
is a cardinal which is n-huge for all finite n" is interpretable in
ESR(epsilon*)#.

The consensus among set theorists is that ZFC + "there is a
nontrivial elementary embedding from some L(V(alpha+1)) into itself"
is consistent.

Finally, consider the following system ESR(epsilon*)##.

if a given sentence of L^2(epsilon) holds in a given category of
elemental classes not forming an elemental class, then it holds in an
elemental subclass and in a nonelemental extensionally proper
subclass.

THEOREM 1.4. ESR(epsilon*)## is mutually interpretable with ZF +
{there exists a Pi-1-n indescribable V(alpha) and a nontrivial
elementary embedding from V(alpha) into V(alpha)}_n. ESR(epsilon*)##
proves the consistency of ZFC + "there is a nontrivial elementary
embedding from some V(alpha+1) into V(alpha+1)".

The last conclusion in Theorem 1.4 uses the above cited results of Woodin.

For the formal presentations of ESR(epsilon*), ESR(epsilon*)#,
ESR(epsilon*)##, let phi be a formula of L(epsilon), and let psi be a
sentence of L^2(epsilon) with no variables in common with phi. Let y
be a variable in phi. We want to define the formula psi[phi,y] of
L(epsilon). For the subclass variables Z in psi, associate object
variables Z', so that the Z' are distinct and do not appear in
phi,psi (and for technical reasons are not x,y). Let psi[phi,y] be
the result of replacing all quantifiers (Qz) in psi by

(Qz|phi[y/z])

and all quantifiers (QZ) in psi by

(QZ'|(forall y epsilon Z')(phi))

and expanding the result to a formula of L(epsilon).

Informally, psi[phi,y] is the (formula expressing the) result of
relativizing all object quantifiers in psi to {y: phi(y)} and all
subclass quantifiers to subclasses of {y: phi(y)}. In particular,
psi[y epsilon x,y] is the (formula expressing the) result of
relativizing all object quantifiers in psi to (the elements of) x,
and all subclass quantifiers to subclasses of x.

ESR(epsilon*) is the formal system in L(epsilon) whose nonlogical axioms are

((forall y)(phi implies E(y)) & psi[phi,y]) implies
(therexists x)(E(x) & (forall y epsilon x)(phi) & psi[y epsilon x,y])

where x,y are distinct variables, phi is a formula of L(epsilon) in
which x is not free, psi is a sentence of L^2(epsilon) with no
variables in common with phi, y is a variable in phi, E(x) is
(therexists y)(x epsilon y), and E(y) is (therexists x)(y epsilon x).

We leave the formalizations of ESR(epsilon*)# and ESR(epsilon*)## to
the reader.

2. ESR(epsilon) and ESRIS(epsilon).

3. ESR(epsilon*).

4. ESR(epsilon*)#.

5. ESR(epsilon*)##.

REFERENCES

[Fr03] Sentential reflection, preprint, January 5, 2003.

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

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

This is the 159th 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
146:Large large cardinals  4/18/02  4:30AM
147:Another Way  7:21AM  4/22/02
148:Finite forms by relativization  2:55AM  5/15/02
149:Bad Typo  1:59PM  5/15/02
150:Finite obstruction/statisics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection