[FOM] Axiomatizing Higher Order Set Theory

[Dmytro Taranovsky]

A key limitation of set theory is that for some properties of sets, 
there is no set of all sets that satisfy the property.  To address this 
limitation, we consider higher order set theory, but immediately hit a 
roadblock:  If V contains all sets, then we cannot form structures above V.

The solution is to build higher-order set theory inside V.  That is, we 
can use a cardinal kappa to represent Ord (the class of all ordinals), 
elements of V_kappa represent sets, subsets of V_kappa -- classes, 
elements of P(P(V_kappa)) -- collections of classes, and so on.  
However, not all cardinals are suitable for this purpose.

Definition:  A cardinal kappa is reflective if it is correct about 
higher order set theory with parameters in V_kappa.

Note:  See below for an alternative equivalent definition that uses 
reflection properties instead of higher order set theory.

This definition cannot be formalized in the language of set theory.  
Instead, we
1. Extend the language of set theory with a predicate R:  R(kappa) <==> 
kappa is reflective.
2. Axiomatize the resulting extension.
3. Argue that the extension is well-defined, or at least has a solid 
conceptual basis.

Let us start axiomatizing.
A1. ZFC
A2. Axiom schema of replacement for formulas involving R.
A3. R(kappa) ==> kappa is an ordinal

Now, while we cannot just formulate correctness for higher order set 
theory as an axiom, the key observation is that if both kappa and lambda 
are correct, then they agree with each other.
A4. (schema, phi has two free variables and does not use R)
R(kappa) and R(lambda) ==> forall s in V_min(kappa,lambda) ( phi(s, 
kappa) <==> phi(s, lambda) ).

Finally, to use reflective cardinals for higher order set theory, we need:
A5. There is a proper class of reflective cardinals

Theorem:  A1-A5 is equiconsistent with ZFC + Ord is subtle.

The axioms for reflective cardinals naturally correspond to the large 
cardinal property of full indescribability:
A6.  Schema (phi has two free variables and does not use R):  If kappa 
is reflective and A is a set, then
phi(kappa, A intersect kappa) ==> thereis lambda<kappa phi(lambda, A 
intersect lambda)

A6 implies that reflective cardinals are strongly unfoldable (==> 
totally indescribable ==> weakly compact ==> Mahlo ==> inaccessible).

Theorem:  A1-A5 implies that A6 holds in HOD.  A1-A6 is Pi^V_2 
conservative over A1-A5.

In our presentation so far, there is still incompleteness about how 
similar elements of R have to be to each other.  While one option would 
be to keep R open-ended and progressively reach higher expressive power 
through stronger indiscernability requirements on elements of R, we 
propose to make R definite by requiring R(kappa) <==> (R union {kappa} 
satisfies A4).  This can be formalized into a single statement, which 
however is slightly technical:
A4a.  forall a R(a) ==> Ord(a) (that is a is an ordinal); forall a,b,c 
(Ord(a) and R(b) and R(c) and 0<a<b<c ==> (R(a) <==> forall 'phi' forall 
s in V_a ( phi(a, s) holds in V_b iff phi(b, s) holds in V_c ))), where 
'phi' ranges over (codes for) formulas in set theory (without R) with 
two free variables.

Theorem:  ZFC + A4a + A5 + "forall s (R intersect s exists)" is finitely 
axiomatizable and implies A4.

A4a slightly increases the consistency strength, which, however, remains 
below subtle cardinals.  A consequence of A4a is that R is definable 
from every proper class S subclass R.  Analogously to A4a, we can 
convert A6 into a single statement (which inherently makes it slightly 
stronger) by using a reflective cardinal in place of V.


It remains to show that R is well-defined, or at least intuitively 
sound.  While V is poorly understood, the constructible universe L is a 
well-understood model of set theory.
Theorem (ZFC + zero sharp):  There is unique R such that (L, in, R) 
satisfies A4a and R holds for a proper class of cardinals (that is 
cardinals in V).  (L, in, R) also satisfies A1-A6.

Moreover, we get the same theorem for other canonical inner models, 
which suggests that there is unique natural way to choose R in V to 
satisfy the axioms, which we intuitively describe as follows.

Key to infinitary set theory is the concept of a reflection property.  
Examples of reflection properties abound -- "kappa is a cardinal", 
"kappa is inaccessible", "kappa is a Sigma-2 elementary substructure of 
V", and so on, and they appear to form a directed system.
Convergence Hypothesis:  If ordinals a and b have sufficiently strong 
reflection properties, then they satisfy the same set of statements, 
even with parameters in V_min(a,b).
Definition (assuming convergence hypothesis):  kappa is a reflective 
cardinal, denoted by R(kappa), iff (V, kappa, in) has the same theory 
with parameters in V_kappa  as (V, lambda, in) for every cardinal lambda 
 > kappa with sufficiently strong reflection properties.

Although the notion of a reflection property is vague, the convergence 
hypothesis (combined with the axiomatization) allows us to escape the 
vagueness, and make the notion of R unambiguous.  While our axioms are 
incomplete, they are not significantly more incomplete than the axioms 
of set theory. Just like ZFC, the theory can be extended with large 
cardinal axioms.  There are natural ways to incorporate large cardinal 
notions at the full expressive level of R, and this sometimes leads to 
stronger large cardinal notions.

The results -- and much more -- are in my paper:
http://web.mit.edu/dmytro/www/ReflectiveCardinals.htm
(also available on arXiv: http://arxiv.org/abs/1203.2270)

As always, I am looking for feedback, whether or not you agree with me.

Sincerely,
Dmytro Taranovsky