Replacement in first order logic

Question

I have a question on something extremely basic I can't find described properly in literature. It must be so obvious most people don't even need to hear about it.

My starting point is this. In first order logic with equality, I have an axiom telling me that I can substitute equal things in formulas. Why isn't there a similar axiom for logically equivalent formulas? Everybody does this kind of substitutions all the time in formal proof, but how are they justified rigorously? Shouldn't there be an axiom?

I have tried to use the existing axioms and here's my attempt. If $\alpha \Leftrightarrow \beta$ and I have a formula $\varphi$ containing $\alpha$, I suppose I could say that $\varphi \Leftrightarrow \varphi'$ is a tautology where $\varphi'$ is $\varphi$ where I have substituted some occurrences of $\alpha$ with $\beta$. My argument (perhaps not too formal) would be that I have not changed any truth tables by substituting. Once I have that tautology, if $\varphi$ holds, I could use biconditional elimination and deduce $\varphi'$.

However, this doesn't quite work when quantifiers are thrown into the mix. If $\varphi \equiv \forall x \alpha$, I can't say that $\forall x \alpha \Leftrightarrow \forall x \beta$ is a propositional tautology.

In a nutshell, does anyone know what it is that justifies swapping logically equivalent formulas in a formal proof?

Answer 1

Yes; we have a "substitution theorem" in FOL.

See: Dirk van Dalen, Logic and Structure, Springer (5th ed. 2013), page 70, for a "bookkeeping lemma" regarding substitution.

With it, we can prove:

$\vDash (ϕ ↔ ψ) → (σ [ϕ/\$]↔σ[ψ/\$])$,

where the “$\$$” symbol is a “place holder” for an atom.

Of course, substitution must be carefully defined in order to avoid "clash" with existing quantifiers; i.e.: $ϕ,ψ$ must be free for $\$$ in $σ$ (see page 61-63).

Answer 2

As long as you restrict yourself to sentences (so all of propositional logic, but also formulas in quantificational logic without any free variables), then these substitutions are indeed perfectly logically valid, and several texts prove a kind of 'Substitution Theorem' or 'Replacement Theorem' to this effect.

Moreover, there are formal proof systems that allow you to do this kind of thing. Some proof systems have a set of predefined logical equivalences (such as Double Negation, DeMorgan, Commutation, Association, Distribution, etc.) that can be used as inferences in a proof (see for example Copi's formal proof systems) and I know I have seen proof systems where any earlier proven equivalence can be used as a 'substitution' inference in other proofs.

When it comes to formulas in general (where you can have free variables) you need to be a little more careful, as you already realized (although I cannot quite follow your example ...). However, we can still a few things as far as equivalences and substitutions go.

First of all, as long as no variables are changed, we can easily extend the propositional logic equivalences to formulas. Thus, we can say that $Happy(x) \Leftrightarrow \neg \neg Happy(x)$, and since we can likewise extend the 'Substitution Theorem' to formulas, we can therefore infer $\forall x \ \neg \neg Happy(x)$ from $\forall x \ Happy(x)$.

When variables are changed, though, things get more tricky. In fact, it may seem that $Happy(x)$ is logically equivalent to $Happy(y)$, but clearly you cannot infer $\forall x \ Happy(y)$ from $\forall x \ Happy(x)$. Fortunately, it turns out that $Happy(x)$ not logically equivalent to $Happy(y)$ anyway, as we define the logical equivalence of formulas in terms of variable assignments (functions that map variables to objects in the domain) and as such I can map $x$ to a different object than $y$, and thereby demonstrate their non-equivalence.

Nevertheless, there still are equivalences that involve changing variables: $\forall x \ Happy(x)$ is equivalent to $\forall y \ Happy(y)$. Indeed, there is a general 'Replacing Bound variables' equivalence principle:

Replacing Bound variables

Where $\varphi(x)$ and $\varphi(y)$ are any FOL formulas, and where $\varphi(x)$ would be the result of replacing all free variables of $y$ in $\varphi(y)$, and where $\varphi(y)$ would be the result of replacing all free variables of $x$ in $\varphi(x)$:

$\forall x \ \varphi(x) \Leftrightarrow \forall y \ \varphi(y)$

$\exists x \ \varphi(x) \Leftrightarrow \exists y \ \varphi(y)$

In sum, then, as long as you have a good definition of logical equivalence of formulas, then there is indeed a general Substitution Principle of exactly the kind you suggest, and you could even make that into a formal inference rule.

Answer 3

Thank you @Bram28. What you wrote made a very interesting read. I'll try to explain to you where it is that I believe I am missing something. Let's assume we get rid of the problem of variables with different names. If I have $\forall y Happy(y)$ and I need $\forall x Happy(x)$, I can easily change the variable before worrying about the logical equivalence with something else. But here's where I get confused. You wrote that $\forall x Happy(x)$ is logically equivalent to $\forall x \neg \neg Happy(x)$. Well, I agree, but in order to prove it I would take several steps and prove that the first implies the second and viceversa by using universal instantiation and generalisation. After doing this, I'd have my result, but it would not be general. Like you, I have seen around proof systems using "rules of replacement", but it looks to me that there is no theorem that lets me use them in a general way. Therefore, your reply lets me formulate my question better. Is there any theorem that lets me substitute, even if under some conditions on variable names some "quantified bits" of a formula, or do I have to do all the work every time? I give you a more sophisticated example:

$\forall x (P(x) \wedge \forall y Q(x,y))$

If I had somewhere in my proof the formula $R(x,y) \Leftrightarrow Q(x,y)$, would there be a theorem that lets me conclude

$\forall x (P(x) \wedge \forall y R(x,y))$

or would I have to play with universal instantiations and generalisations until I manage to prove it?

Answer 4

My argument (perhaps not too formal) would be that I have not changed any truth tables by substituting. … However, this doesn't quite work when quantifiers are thrown into the mix. If $\varphi \equiv \forall x \alpha$, I can't say that $\forall x \alpha \Leftrightarrow \forall x \beta$ is a propositional tautology.

Well, it is possible to make your argument formal and extend it to first-order logic. Truth tables belong to model theory, and there are corresponding definitions for quantifiers. However, proving it by model theory is a detour. A usual proof system (inference system) is sufficient. You use something to reason about quantifiers, right? Truth tables do not handle quantifiers.

Shouldn't there be an axiom?

There is no need for additional axioms. It can be proved from the usual proof system. Here is the proof idea. Do structural recursion on $\phi$. For the case $\phi = \forall x\psi $, $\psi\leftrightarrow\psi'$ is an induction hypothesis, use a theorem scheme $\forall x(\psi\leftrightarrow\psi') \to (\forall x\psi\leftrightarrow\forall x\psi')$.

A proof of $\forall x(\psi\leftrightarrow\psi') \to (\forall x\psi\leftrightarrow\forall x\psi')$ using natural deduction. Suppose $\forall x(\psi\leftrightarrow\psi')$. [Suppose $\forall x\psi$. [Let $x$ be given. Apply $x$ to $\forall x\psi$ and obtain $\psi$. Apply $x$ to $\forall x(\psi\leftrightarrow\psi')$ and obtain $\psi\to\psi'$. By modus ponens, $\psi'$.] Hence $\forall x\psi'$.] Hence $\forall x\psi\to\forall x\psi'$. $\forall x\psi'\to\forall x\psi$ by symmetry. Hence $\forall x\psi\leftrightarrow\forall x\psi'$. $\square $

Existential quantifiers may be defined via universal quantifiers ($\exists x\phi := \lnot\forall x\lnot\phi $) or handled by a similar theorem scheme. You can find a detailed proof for a Hilbert-style proof system in “Introduction to Mathematical Logic” by Elliott Mendelson, 6th edition, Proposition 2.9.