[FOM] Higher Order Set Theory and ZFC

[Dmytro Taranovsky]

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