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?