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