[FOM] n-th order ZFC
Roger Bishop Jones
rbj at rbjones.com
Thu Jul 7 02:24:07 EDT 2011
On Tuesday 05 Jul 2011 20:23, pax0 at seznam.cz wrote:
> Is there ANY USEFUL SITUATION which would mention
> n-th order ZFC
> for n>=3?
I work in higher order set theories using a polymorphic
version of Church's higher order logic which is logically
equivalent (or stronger than) omega-order ZFC.
There are practical advantages in having objects of higher
than second order even in the formalisation of ZFC in HOL,
and if you then want to make use of this formulation the
orders soon stack up.
For the most simple example, in formalising ZFC in HOL the
constant for union has type: SET -> (SET -> SET) which is
already of order greater than 2.
There is a formulation of this kind at:
if you look at the theory listings in section 7 onwards the
constants defined and their types are shown.
The kinds of foundational application of this theory which I
engage in involve further constructions over this universe
of sets, and introduce objects of even higher type.
For example see:
in which an infinitary combinatory logic is constructed using
this higher order set theory.
Of course, it remains moot whether this constitutes a USEFUL
SITUATION!, and there is no suggestion here that the use of
omega order set theory is essential rather than merely
More information about the FOM