[FOM] Higher Order Set Theory

[Roger Bishop Jones]

On Monday 07 March 2005  3:39 pm, Dmytro Taranovsky wrote:
> Since the universe includes all sets, second order statements
> about V appear doubtful or meaningless.  However, there is a
> way to make them meaningful, and to get a reasonable
> axiomatization of theory, thus resolving how to deal with
> proper classes, "collections" of proper classes, and proper
> class categories such as the category of all groups.

Higher order set theory is a great deal less problematic than
you make it appear.
I have done work in higher order (omega-order) set theory
on and off since 1988 using the theorem provers HOL and
ProofPower, but there are much earlier uses in the literature.
I believe Carnap did some work in higher order set theory
though I can't offer a reference.

As far as metatheory and semantics is concerned, higher order
set theory is hardly more problematic than first order
set theory.
"V", the universe of ALL sets is just as much a problem in
the metatheory of first order set theory as in higher order
set theory.
All the other less controversial models of
first order set theory (e.g. the V(alpha) for alpha inaccessible)
extend to models of w-order set theory (which may or may not be
"standard" models).

As far as axiom systems are concerned, ZFC can straightforwardly
be transcribed into higher order logic, replacing axiom 
schemata by axioms quantifying over sets, if you don't mind
(or actually want) something stronger than ZFC.
Francisco Corrella wrote a PhD (back in the eighties)
which addressed higher order set theories which were no
stronger than first order set theory
(though I never understood the motivation for this).

Perhaps you could explain what you think is wrong with
these obvious ways of doing higher order set theory
(apart from losing V as a model).

Roger Jones