4
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ Or if I were to add such a rule to FOL, would that be an extension of FOL (which basically makes the predicate symbols some sort of predicate variables)? and would it be a conservative extension of FOL? $\endgroup$ – JuneA Jul 26 '15 at 17:56
  • $\begingroup$ For the 2nd ... this is Second Order Logic. $\endgroup$ – Mauro ALLEGRANZA Jul 26 '15 at 19:52
  • $\begingroup$ Then I don't understand how the extended FOL would be second order logic, since formulas like $\forall P \exists Q(...)$ would not be wff (I have not extended FOL for this). Rather, it seems that the extended FOL would be to second order logic what PC is to second order propositional logic. $\endgroup$ – JuneA Jul 26 '15 at 21:05
  • $\begingroup$ Substitution of predicates as you ask about is guaranteed to work by the fact that the logical axioms (I'm going to assume an axiomatic presentation) are defined to be substitution instances of certain schemata (and it is completely unrelated, as you guess, to quantification over predicates). I think what you're wondering is whether there's a specific rule of inference that lets you use that sort of substitution as a line of a proof, and there's generally not, for the reason that you can always write down a logical truth (wrt whatever logical system you're using) as a line in your proof. $\endgroup$ – Malice Vidrine Jul 26 '15 at 23:41
  • $\begingroup$ @MaliceVidrine: I don't quite understand your last point. What would be the truth that I would just write down without justification? I think that, after proving the FOL theorem from the question, I would write down its substitution instance and justify this line by the meta-theorem from the answer below (meta-theorem which presumably has been proved in advance). If this is correct then I'm ok. $\endgroup$ – JuneA Jul 28 '15 at 0:26
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I was only considering $\mathbf{\vdash S}$ implies $\vdash ({Q_{x_1 \dots x_n} / p})\mathbf{S}$. This can be proved by showing that, if $\mathbf{S}$ is valid in all models, then so is $({Q_{x_1 \dots x_n} / p})\mathbf{S}$, and by completeness the latter is a theorem. Your rule is stronger, but I guess it can be proved in a similar way and with the help of the deduction theorem, correct? $\endgroup$ – JuneA Jul 27 '15 at 23:52
  • $\begingroup$ One basically uses an induction. The entailment relation $\vdash$ is the smallest relation satisfying various rules. Defining $R \vdash_{(Q_{\underline x}/p)} S$ as $(Q_{\underline x}/p) R \vdash (Q_{\underline x}/p) S$, roughly the idea is to show that $\vdash_{(Q_{\underline x}/p)}$ satisfies all the rules and so defines a larger relation than $\vdash$. But substitutability can fail, which one may get around, basically, by instead showing first that substituting variants into variants yields variants when it's all defined, and then doing a similar induction where variants are identified. $\endgroup$ – Stephen A. Meigs Jul 28 '15 at 13:40
  • $\begingroup$ It would be useful to have the full proof available somewhere for reference. Is it true that this cannot be proven from syntax alone? i.e. that one needs to use semantics and completeness to prove this? $\endgroup$ – JuneA Aug 1 '15 at 14:22
  • $\begingroup$ The proof I would suggest is purely syntactical. The result you considered is basically the same, because $R \vdash S$ is equivalent to $\top \vdash R \rightarrow S$, though I tend to think it best to write things to emphasize preorder nature of $\vdash$. Notice that the result elegantly has as immediate corollary that extensions via predicate symbol are conservative and translatable. One also doesn't need completeness to show one may substitute analogously for function symbols. But completeness results seem to become quite useful in showing extensions via function symbol are conservative. $\endgroup$ – Stephen A. Meigs Aug 4 '15 at 16:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.