[FOM] 158:Sentential Reflection
Harvey Friedman
friedman at math.ohio-state.edu
Mon Mar 31 00:17:10 EST 2003
A PDF version of this abstract will be available in a few days on
http://www.mathpreprints.com/math/Preprint/show/
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
January 5, 2003
Abstract. We present two forms of "sentential reflection", which are
shown to be mutually interpretable with Z_2 and ZFC, respectively.
1. Introduction.
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.
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.
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).
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.
The first version of sentential reflection that we consider is
SR(epsilon), which informally asserts the following.
if a given sentence of L(epsilon) holds in a given category
then it holds in a subclass.
Here "holds in" means that it holds if the quantifiers are
relativized over the category or class.
THEOREM 1.1. SR(epsilon) is mutually interpretable with Z_2.
See [Si99] for copious material on Z_2, which is the standard two
sorted first order system for "second order arithmetic".
Z_2 is much weaker in interpretation power than ZFC. In particular,
ZFC is not interpretable in SR. So in order to achieve mutually
interpretability with ZFC, we strengthen the choice of language.
One way of strengthening SR(epsilon) is to strengthen the notion of "subclass".
We say that the class x is an inclusion subclass of the category K if
and only if
x is a subclass of K, and any element of K
that is a subclass of an element of K lies in x.
This can be restated by a single clause as follows.
any subclass of any element of x lies in K
if and only if it lies in x.
SRIS(epsilon) informally asserts the following.
if a given sentence of L(epsilon) holds in a given category
then it holds in an inclusion subclass.
Here SRIS(epsilon) is read "sentential reflection by inclusion
subclass for L(epsilon)".
THEOREM 1.2. SRIS(epsilon) is provable in ZF and interprets ZFC.
For the formal presentations of SR(epsilon) and SRIS(epsilon), let
phi be a formula of L(epsilon), and let psi be a sentence of
L(epsilon) with no variables in common with phi. Let y be a variable in
phi. Let psi[phi,y] be the result of replacing all quantifiers (Qz)
in phi by
(Qz|phi[y/z])
and expanding the result to a formula of L(epsilon).
Informally, psi[phi,y] is the (formula expressing the) result of
relativizing all quantifiers in psi to {y: phi(y)}. In particular,
psi[y epsilon x,y] is the (formula expressing the) result of
relativizing all quantifiers in psi to (the elements of) x.
SR(epsilon) is the formal system in L(epsilon) whose nonlogical axioms are
psi[phi,y] implies (therexists 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(epsilon) with no
variables in common with phi, and y is a variable in phi.
SRIS(epsilon) is the formal system in L(epsilon) whose nonlogical axioms are
psi[phi,y] implies (therexists x)((forall y containedin z epsilon
x)(phi iff y epsilon x) & psi[y epsilon x,y])
where x,y,z are distinct variables, phi is a formula of L(epsilon) in
which x,z are not free, psi is a sentence of L(epsilon) with no
variables in common with phi, and y is a variable in phi.
2. SR(epsilon).
3. SRIS(epsilon).
*********************************************
I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 158th 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
More information about the FOM
mailing list