# [FOM] Higher Order Set Theory and ZFC

Dmytro Taranovsky dmytro at mit.edu
Wed Apr 18 18:44:17 EDT 2012

```Since ZFC is the current standard set theory (that is by default,
provability means provability in ZFC), a question arises as to what
extent can higher order set theory be formalized in a theory
conservative over ZFC.  A well-known theory conservative over ZFC is
obtained by adding a symbol kappa and schema "V_kappa is an elementary
substructure of V".  However, we can go much further than that:
- we can have multiple cardinals representing Ord instead of just kappa, and
- we can iterate the notion of higher order set theory any finite number
of times.

Recall from my paper (and my FOM postings)
http://arxiv.org/abs/1203.2270
that for a definable predicate X, a cardinal kappa is X-reflective iff
the theory (V, in, X, kappa) with parameters in V_kappa agrees with the
theory of (V, in, X, lambda) for every lambda>kappa with sufficiently
strong reflection properties.  R_1 is the predicate for reflective
cardinals and R_{n+1} is the predicate for R_n-reflective cardinals.

The natural basic theory of R_{n+1} has consistency strength between
n-ineffable and n+1-subtle, but there is a substantial fragment that is
conservative over ZFC, defined as follows.

The language consists of the language of ZFC (first order logic and
membership relation), and predicate R_i for every positive integer i.
The axioms are
(1) ZFC, plus replacement for formulas in the extended language
(2) (schema, n>0) there is cardinal kappa satisfying R_n(kappa)
(3) (schema, n>0) R_{n+1}(kappa) ==> R_n(kappa)
(4) (schema, n>0, and elementarity is also a schema) R_n(kappa) implies
that (V_kappa, in, R_1, ..., R_{n-1}) is an elementary substructure of
(V, in, R_1, ..., R_{n-1}).
(5) (schema, n>=0, phi is a formula in (V, in, R_1, ..., R_n) with two
free variables, and S is a set definable in (V, in , R_1, ..., R_n))
R{n+1}(kappa) and R_{n+1}(lambda) ==> forall s in S (phi(kappa,s) <==>
phi(lambda,s)).

[Note: In (5), the schema over S is interpreted as schema over formulas
psi in (V, in, R_1, ..., R_n}) with one free variable, using S = {s:
psi(s)} and with the main statement conditioned on S being a set.]

Conservation over ZFC is proved by showing that given a finite fragment
of the theory, R_i (for every used i) can be defined in ZFC so as to
satisfy the fragment.

(4) and (5) try to assert that elements of R_{n+1} are correct for
higher order set theory with R_1, ..., R_n.  (4) asserts that V_kappa is
similar to V.  (5) asserts that (since kappa and lambda are both correct
for higher order set theory with R_1,...,R_n) cardinals satisfying
R_{n+1} agree with each other.  However, being conservative over ZFC
imposes strict limitations on how far we can go.  For example, in (5),
we are using S instead of V_min(kappa,lambda).

Another limitation of being conservative over ZFC is that in this
theory, we cannot define R_n from R_{n+1}.  However, (4) combined with
(2) and (3) ensures that there are many cardinals satisfying R_n.

If the axioms are extended to include R_1(kappa) ==> "kappa is regular",
then the resulting theory is conservative over ZFC + (schema) "Ord is
Mahlo", and analogously with other properties besides regularity.  (In
ZFC, "Ord is Mahlo" is equivalent to (schema) there is regular kappa
such that V_kappa is a Sigma_n elementary substructure of V.)

Sincerely,
Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm
```