# Generalized Formal First Order Logic

I am doing some research into logic, I have gotten far into Propositional Calculus and its generalizations, my issue comes when I go into Predicate Calculus.

I am trying to look into it in a more generalized sense and not the specific one we are using most commonly. So for quantifiers I consider things beyond $\forall$ (and by extension $\exists$)

I understand we can subdivide the "alphabet" of GFOL (Generalized First Order Logic) accordingly

Variables $V_i$, Function $F_i^k$, Predicates $P_i^k$, Operators/Connectors, $O_i^k$ and Quantifiers, this is where I get uncertain, does it have an arity? Imma assume here no but please correct me! $Q_j$.

I know that terms are inductively defiend as this

• $V_i$ are Terms
• If $T_i$ is a term, then $F_i^k(T_1,\ldots,T_k)$ is a term.

and for WFF they are also defined inductively. Let $T_i$ be terms as before and $W_i$ be a WFF.

• $P^k_i(T_1,\ldots,T_k)$ is a WFF.
• $O_i^k(W_1,\ldots,W_k)$ is a WFF
• $Q_i V_j W_k$ is a formula

I feel secure with the Term one, but WFF one I do not as I am not certain how to generalize quantifiers, if they are all unary it would be done but are they always unary in FOL?

I next consider substitution for these things, that is $A[B/x]$. I understand the general idea of it but looking at This it only speaks about existential quantifier, but how would I generalize it to a general quantifier $Q_i$? Are there any good sources for this?