Rules of stratified high order logic are:
Terms:
1.Variable symbols that range over all predicates.
so P, when written alone, is taken to range over all predicates, but when P is coupled with a string of variables like in P(Q1,..,Qn) then P would be restricted
to range over all n-ary predicates. [More correctly: P in P(Q1,..,Qn) still range over all predicates but the formula P(Q1,..,xn) can only be true if P is an n-ary predicate, since otherwise it would be clearly false, however anothree approach is to restrict the whole logic to unary predicates, of course high order, so the variables in this langauge range over all and only unary variables (15 Aug. 2020)].
Formula formation rules: all rules of propositional logic
+
if P is term, and Q1,..,Qn are variable terms, then P(Q1,..,Qn) is a FORMULA.
If P(Q1,..,Qn) is a formula then for all P (Q1,..Qn)
, Exists P(Q1,..,Qn) are formulas.
+
All formula formation rules of FOL.
Care must be taken to limit P to the same arity in a formula, so all occurrences of P that are quantified by the same quantifier must be of the same arity, for example $\exists P, Q1,..,Qn (P(Q1) \land P(Q1,Q2)) $ this is not a formula of the language. [Aug 14,2020]
Rules of Inference: Modus-Ponens, rules of quantification
as present in first-order logic.
Axioms:
1. Stratified Predication: if phi is a stratified higher-order formula that does not use the symbol P, then
Ax1,..,xn EP Ay1..ym(P(y1,..,ym) <-> phi(y1,..,ym,x1,..,xn))
is an axiom.
2. Extensional Predication:
Ax1,..,xn[Q(x1,..,xn) <-> P(x1,..,xn)] -> Q=P
A stratified formula phi is a formula in higher order language whereby a function f can be stipulated in a recursive manner over variables in phi such that for
each atomic n-ary subformula P(Q1,..,Qn) of phi we have:
f(P)= (f(Q1),..,f(Qn))
i.e. the type assigned to P by f is the tuple of types
assigned to each of its arguments by f.
[writing at Aug 13, 2020] I don't know why I've stipulated typing in that way at then. I now think its enough to say that for any atomic formula P(Q1,..,Qn) All of Q_1,..,Q_n are assigned the SAME type, and P is assigned one type higher than the type of its arguments.
In this kind of logic one can DEFINE identity as:
x=y <=df=> AP (P(x) <-> P(y))
where P is a UNARY predicate symbol.
In my opinion, it appears to me that this logic is purely logically motivated! the stratification criterion clearly resolves confusion about the LEVEL of predication so it prevents a predicate symbol appearing at two different LEVELS of predication, which is a logical motivation. Also, Extensionality is dependent on the idea that "predication" is all of what is there for predicates, to go against it is to say that predicates have other constituents not related to their predication role, which would be extremely non-plausible.
I personally don't see a clear SET based motivation for this theory, although it might indeed be interpreted in that manner. It appears that this theory would collapse into NF. But even so, this doesn't mean that it is primarily motivated by NF. On the contrary, actually, this logical framework is more natural as regards stratification than is the set milieu of NF. It is this logic that could provides a motivation for NF and not the other way round.
The provision of a definition of identity in a purely based logical theory DOES provide a basis for regarding identity as a LOGICAL CONSTANT.
Notes [Aug 14, 2020]: Not only identity is definable in this logic, even set membership is clearly definable, this would be:
x E y <-> y(x)
So sets are nohting but unary predicates, and set membership is fulfillment of those predicates.
The main problem with this logic is that its consistency depends heavily on that of NF.
A more plausible line [logically speaking] is to have a bottom tire of OBJECTS, now those would behave as Ur-elements with respect to the defined set membership relation E. By then we'd have it of the strength of NFU. Which is pretty much weak. However if we add an axiom of infinity to that logic (thereby in some sense endangering its 'logical' nature, since it would be thought of as mathematical rather than a pure logical theory), then we get it to the strength of NFU+ Infinity.
Also this theory lacks choice, which should be added to it. However this theory without infinity and choice is still strong, it can interpret Robinson's arithmetic Q in it, and so it cannot be complete!
Zuhair