[FOM] n-th order ZFC

[Roger Bishop Jones]

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:

rbjones.com/rbjpub/pp/doc/t042.pdf

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:

rbjones.com/rbjpub/pp/doc/t041.pdf

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 
convenient.

Roger Jones