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?
Thank you in advance.