Typed Extensional logic and PA

[Zuhair]

A typed predicate symbol is a predicate symbol labeled after its
order.

So P_i mean the i_th order predicate.

Now typed predicates when definable must be defined after a typed
formula which is a formula in which all predicates are also typed in a
manner delineating their order.

For example the predicate Q definable after "Exist P. P(x) & ~P(y)" ,
this formula is untyped since P ranges over all kinds of predicates
whether definable after first order or second order formulas.

While the formula "Exist P1. P1(x) & ~P1(y)" is a typed second order
formula.

Now we'll maintain that Extensions of predicates are only possible if
they are definable after typed formulas or otherwise being primitive
first order predicates, i.e. only fulfilled by objects.

Typing of predicates is stipulated recursively we start with primitive
predicates having objects as their arguments, those are labeled as
typed first order predicates, then also we'll have definable typed
first order predicates those are definable after formulas in which no
quantification occurs over predicate symbols, now typed second order
predicates are those definable after formulas having quantification
over objects or typed first order predicates, etc....

Accordingly I'll propose the following:

If Pi is a typed predicate then, ePi is a term.

Axiomatize:

i=1,2,3,..., j=1,2,3,....
ePi = eQj iff (for all x. Pi(x) <-> Qj(x))

ePi is read as the "extension of Pi"

Then define 'membership' in an untyped manner as:

x E y iff Exist P. P(x) & eP=y

Notice that a binary predicate symbol E has been defined in untyped
manner to mirror "fulfillment" of predicates in the object world.

However it is nice to see that this system doesn't entail that the
predicate E can have an extension, so we are not forced to have
something like eE, because E is untyped. This is important because the
'fulfillment' of predicates is itself not a predicate, the article
"is" in Socrates is a man, and also in white is a color, is an
'assertion' and not a predicate, so "is" doesn't have an extension to
represent it. This is acceptable I think. Similarly the relation E
defined to parallel "is" in predication must not have an extension
since "is" is not a predicate.

I call the above Typed Extensional Logic "TEL". And I consider it as
"logic" since I don't see a clear 'extra-logical' concept involved. So
if PA is interpreted in TEL
then clearly PA is logical!

Zuhair