In a Hilbert-style axiomatization of first-order logic (FOL), there is a rule for variable substitution but I don't see any rule for substituting predicate symbols. Consider a theorem like:
$\forall x(P(x)) \lor \forall x(Q(x)) \rightarrow \forall x(P(x) \lor Q(x))$
Intuitively I would think that I should be able to substitute $\lnot P(x)$ for $P(x)$ in the above and still get a valid formula (since the theorem was valid under all interpretations to begin with). Even more, I may want to substitute, say, $P(x)\land Q(x)$ for $P(x)$ and $P(x)\leftrightarrow Q(x)$ for $Q(x)$ if it were allowed.
In propositional calculus (PC) there is the rule of uniform substitution for propositional symbols, which could be considered predicates of arity 0. But in FOL this rule seems to be "burried" by defining all PC tautologies as an axiom schema, and then apparently I can no longer apply the rule.
So is it possible to define such an admissible (derivable?) rule for uniform substitution of predicate symbols in FOL? If yes, what would be the rule in the most general case and how would one prove it? If no, can you give an example where the application of such a rule to a provable formula would result in an invalid formula, or perhaps why it does not make sense to have such a rule?
One could try defining the statement $\mathbf{({Q_{x_1 \dots x_n} / p})R}$ (where $\mathbf{p}$ is $n$-ary) as the statement obtained by simultaneously replacing in $\mathbf{R}$ all occurrences of terms of the form $\mathbf {p a_1 \dots a_n}$ with $\mathbf{{{Q}_{x_1 \dots x_n}}(a_1, \dots, a_n)}$. For this to be defined, one needs all the $\mathbf{a_i}$ to be substitutable for $\mathbf{x_i}$ in $\mathbf{Q}$ on the one hand, and on the other, one needs that no variable which is free in $\mathbf{Q}$, except possibly the variables $\mathbf{x_1,..., x_n}$, is a quantifier in $\mathbf{R}$ that includes $\mathbf{p}$ in its scope (trivial when $\mathbf{Q}$ contains no variables freely beside the $\mathbf{x_i}$).
If these substitutability conditions hold, then it's a metatheorem that $\mathbf{R \vdash S}$ implies $\mathbf{({Q_{x_1 \dots x_n} / p)R} \vdash ({Q_{x_1 \dots x_n} / p})S}$.
I don't know why this substituting for predicate symbols (and function symbols) isn't formally covered in others' logic books that I have seen. I guess they think it's too obvious to be worth their bother.