Is this kind of high order logic of individual predicates inconsistent?

Lets permit quantification over predicate symbols in formulas, so the formula formation rules would the same as those of first order logic, but with allowing quantification over predicates, and allowing predication over predicates, so if $$P$$ is a predicate and $$Q$$ is a predicate, then $$P(Q)$$ is a formula.

lets add a primitive unary predicate notion $$ind$$, denoting "individual". This logic extends first order predicate logic, so it has all of its axioms and inference rules. However, existence of predicates after formulas is not unleashed, i.e. we don't have a rule stating that if $$\psi$$ is formula, then there exists a predicate $$P$$ that predicates all and only what fulfills $$\psi$$, rather the monadic predicate existence rules are the following.

Monadic Predicate existence axiom schema:if $$\psi(Q)$$ is a purely logical formula [i.e., doesn't use the symbol ind] in which $$Q$$ is free, having its parameters among $$\vec{A}$$, then all closures of:

$$ind(\vec{A}) \wedge \forall Q (\psi(Q) \to ind(Q)) \to \\\exists P \forall Q (P(Q) \leftrightarrow \psi(Q))$$; are axioms.

In English: If a pure logical formula is closed on individuals, then it defines a predicate.

Axiom of individual predication: $$\forall P (\neg \forall Q(P(Q) \leftrightarrow ind(Q)) \to [ind(P) \leftrightarrow \forall Q (P(Q) \to ind(Q))])$$

In English: any predicate not equivalent to the predicate "individual", is an individual if and only if all of what it predicates are individuals.

Axiom of existence of individuals: $$\exists P,Q [\neg \forall X (P(X) \leftrightarrow Q(X)) \wedge ind(P) \wedge ind(Q)]$$

In English: Two non-equivalent predicates exists.

I'm not sure if this kind of logic is consistent, but if so, then it would interpret that set theory, and so it interprets all of $$ZFC$$.

Question: Is there a serious error with this kind of high order logic?

If not, then had this been studied before?

• This question can't be answered is you don't give some information about the axioms or rules for dealing with the logical connectives in your proposed system. What is the motivation and background for your proposal? – Rob Arthan Feb 19 at 21:19
• it has the same logical rules of first order logic, it only adds to them the axioms depicted above, and also allows quantification over formulas. and specify predicate existence rules after formulas of that language. – Zuhair Feb 19 at 21:26