[FOM] Axiomatizing Higher Order Set Theory

[Dmytro Taranovsky]

Some readers were concerned that the argument in my previous posting for
reflective ordinals (informally, ordinals that are "like" the class of
ordinals, Ord) is not sufficiently persuasive.  However, the language of set
theory was accepted not because all doubts about set-theoretical truth were
dispelled, but because it filled an epistemological need, had a good philosophy
behind it, and had a reasonable (and consistent) axiomatization.  

At the least, axiomatization turns the concept of reflective ordinals into a
valid formal theory. It also makes it easier to debate the existence of
reflective ordinals, and makes reflective ordinals and hence higher order set
theory usable by mathematicians.

Reflective ordinals are regular and hence inaccessible.  Existence of Sigma_n
correct inaccessible cardinals for all n makes Ord appear Mahlo, so reflective
ordinals should be Mahlo.  One can go on justifying more large cardinal
properties for reflective ordinals.

        Reflective ordinals are best axiomatized using elementary embeddings. 
Let R be the predicate for reflectiveness.  Take an image of the universe and
imagine some sets on top of it.  Let j be an elementary embedding of the
extended image with kappa (representing Ord) its critical point.  V(kappa) has
the same theory as j(V(kappa)), and kappa is like a reflective ordinal in
j(V(kappa))--more precisely, it is possible that kappa acts as a reflective
ordinal.  In that case, we use kappa to define reflectiveness restricted to
kappa:  R_j(lambda) iff lambda \in kappa and for all x in V(lambda),
Theory(j(V(kappa)), \in, lambda, x) = Theory(j(V(kappa)), \in, kappa, x).  By
elementarity of j, R_j defines reflectiveness for V(kappa).  If for every
appropriate (V, kappa, j), phi holds in (V(kappa), \in, R_j), the phi.
        The idea can be formalized at the level of indescribable cardinals, but
my formalization is ZFC + For every statement phi, the statement:  
If ZFC proves that for every extender with a critical point kappa, (V(k), \in,
R_j) satisfies phi (where j is the corresponding elementary embedding of V into
M), then phi.

Under the assumption that there are no measurable cardinals, the formalization
is relatively complete (at least with respect to large cardinal structure).  If
there are measurable cardinals, then the formalization could be strengthened
guided by the fact that reflective cardinals satisfy all genuine large cardinal
properties that are realized in V (and are expressibe in ordinary first order
set theory).

Dmytro Taranovsky