Re: Peano arithmetic and simple type theory

On Jun 8, 7:12 am, kleptomaniac6...@xxxxxxxxxxx wrote:
Okay, I made this thread because I had some questions about simple
type theory that were too off-topic for other threads. It seems formal
systems such as the various systems Z, ZF, NBG, are more famous and
more discussed than systems of type theory.

It was briefly discussed in another thread the system that would be
got by joining first order Peano arithmetic and second order induction
to simple type theory, the so called "omega order arithmetic" or OOA.
This would be like taking second order arithmetic, and adding the
apparatus for third order arithmetic, and fourth order arithmetic, ad
infinitum.

Looking up simple type theory on wikipedia, there is a type theory
system which is apparently "simple" "primarily because all members of
the domain and codomain of any relation must be of the same type".
Then what exactly is meant by "simple"?


Remember when I was discussing the distinction between simple and
ramified type theory with you?

In ramified type theory, the classes of individuals are stratified
into different orders. A class defined by a formula with a quantifier
that ranges over individuals is of the first order. A class defined by
a formula with a quantifier that ranges over classes of the first
order is of the second order. And so on. With simple type theory you
haven't got this additional structure, you just have one type of
classes of individuals with the full axiom schema of comprehension for
this type.

.