FOM: 155:A way out

[Harvey Friedman]

I completed a manuscript titled "A Way Out" with full proofs of the claims
a) - f). All looks well. It still needs some final checking before I put it
on the preprint server that I use and submit for publication.

A WAY OUT
Harvey M. Friedman
August 11, 2002

ABSTRACT. We present a way out of Russell's paradox in the form of a direct
weakening of the usual inconsistent full comprehension axiom scheme which,
with no additional axioms, interprets ZFC. In fact, the resulting axiomatic
theory 1) is a subsystem of ZFC + "there exists arbitrarily large subtle
cardinals", and 2) is mutually interpretable with ZFC + the scheme of
subtlety.

1. NEWCOMP.

Bertrand Russell [Ru1902] showed that the Fregean scheme of full
comprehension is inconsistent. Given the intuitive appeal of full
comprehension, this inconsistency is known as Russell's Paradox. The modern
view is to regard full comprehension as misguided, and thereby regard
Russell's Paradox as a refutation of a misguided idea.

We first give an informal presentation of the axiom scheme investigated in
this paper. Informally, the full comprehension axiom scheme in the language
L(epsilon) with only the binary relation symbol epsilon and no equality, is


Every virtual set forms a set.

We use the term "virtual set" to mean a recipe that is meant to be a set,
but may be a "fake set" in the sense that it does not form a set. The
recipes considered here are of the form {x: phi}, where phi is any formula
in L(epsilon).

Other authors prefer to use the term "virtual class", reflecting the idea
that {x: phi} always forms a class, with the understanding that x ranges
over sets. Our terminology reflects the intention to consider only sets,
and construct a powerful set existence axiom.

We say that {x: phi} forms a set if and only if there is a set whose
elements are exactly the y such that phi. Here y must not be free in phi
(and must be different from x). Thus {x: phi} forms a set is expressed by

(therexists y)(forall x)(x epsilon y iff phi).

Russell showed that

{x: x notin x} forms a set

leads to a contradiction in pure logic.

Our way out of Russell's Paradox is to modify the inconsistent Fregean
scheme in this way:

Every virtual set forms a set, or _____.

We refer to what comes after "or" as the "escape clause". The escape clause
that we use involves only the extension of the virtual set and not its
presentation.

We are now ready to present the comprehension axiom scheme.

NEWCOMP. Every virtual set forms a set, or, outside of any given set, has
two inequivalent elements, where all elements of the virtual set belonging
to the first belong to the second.

To avoid any possible ambiguity, we make the following comments (as well as
give a formal presentation in section 2).

1. For Newcomp, we use only the language L(epsilon), which does not have
equality.
2. Here "inequivalent" means "not having the same elements".
3. The escape clause asserts that for any set y, there are two unequal sets
z,w in the extension of the virtual set, neither in y, such that every
element of z in the extension of the virtual set is also an element of w.

We will show that

a) Newcomp is provable in ZFC + "there exists arbitrarily large subtle
cardinals";
b) Newcomp is provable in ZFC + V = L + SSUB, where SSUB is what we call
the scheme of subtlety;
c) Newcomp and ZFC + SSUB are mutually interpretable;
d) Newcomp is interpretable in ZFC + "there exists a subtle cardinal", but
Newcomp is not provable there, assuming that the latter is consistent;
e) all of the above are provable in the weak fragment of arithmetic EFA
(exponential function arithmetic);
f) Newcomp and ZFC + SSUB are equiconsistent, in the sense that their
consistencies are provably equivalent in EFA.

As usual, ZFC is formulated with equality; i.e., in the language L(epsilon,=).

The interpretation of ZFC + SSUB in Newcomp presented here (or coming out
of here) takes the following form (when straightforwardly adjusted). Sets
in ZFC + SSUB are interpreted to be sets in Newcomp. Membership and
equality between the sets in ZFC + SSUB are interpreted as two separate
relations between sets in Newcomp defined by two separate formulas with
exactly two free variables (no parameters). As normally required of
interpretations, the usual connectives and quantifiers are interpreted
without change. Every theorem of ZFC + SSUB becomes a theorem of Newcomp
when so interpreted.

There is an appropriate sense in which this interpretation is a well
founded interpretation. Specifically, it is provable in Newcomp that every
set has a minimal element under the above interpretation of the epsilon
relation of ZFC + SSUB. We can then draw conclusions such as conservative
extension results in the form: any sentence of a certain kind provable in
ZFC + SSUB is provable in Newcomp. However, the statement of such results
involves various coding apparatus available in Newcomp, and we do not go
into this matter here. Suffice it to say that, in an appropriate sense,
every arithmetical theorem of ZFC + SSUB is a theorem of Newcomp (and vice
versa).

In the interpretation of Newcomp in ZFC + "there exists a subtle cardinal",
the sets in Newcomp are interpreted to be some portion of the sets in ZFC +
"there exists a subtle cardinal", (an initial segment, possible proper, of
the constructible hierarchy), and membership between sets in Newcomp is
interpreted as membership between sets in ZFC + "there exists a subtle
cardinal". As normally required of interpretations, the usual connectives
and quantifiers are interpreted without change. Every theorem of Newcomp
ZFC + SSUB becomes a theorem of ZFC + "there exists a subtle cardinal" when
so interpreted.

Of course, when interpreting Newcomp in ZFC + "there are arbitrarily large
subtle cardinals", we can use the identity interpretation, since Newcomp is
provable there.

The system ZFC + SSUB has logical strength a shade below that of ZFC + SUB,
where SUB is "there exists a subtle cardinal", and substantially stronger
than the well studied cardinals below subtle cardinals, such as Mahlo,
weakly compact, or indescribable cardinals. In the well known Chart of
Cardinals in [Ka94], p. 471, subtle fits strictly below kappa arrows omega,
and strictly above "indescribable", well within the cardinals that are
compatible with V = L.

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

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

This is the 155th 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