Peano arithmetic and simple type theory

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"?

I understand that in OOA you do not allow the set of all numbers and
sets of numbers, for example - you are only allowed to quantify over
one type at a time. However, if one does not define ordered pairs in
terms of sets, and treats them instead as primitive, could one not
have, for example, a binary relation whose domain is the set of
natural numbers and whose codomain is the set of all sets of natural
numbers? If n-tuples and sets are treated as fundamentally distinct,
is there anything wrong with this?

.

Quantcast