Analogous to the substitution rule for the equality symbol in FOL, it looks natural to have a substitution rule for the $\leftrightarrow$ symbol in propostional logic, i.e., from the formula …A… and A$\leftrightarrow$B, we can derive the formula …B… I wonder why I did not see it in a logic book. Some books give the $\leftrightarrow$ elimination rule, i.e., from A$\leftrightarrow$B, we can derive $(A \to B)\land(B\to A)$. I wonder if the substitution rule can be replaced by the $\leftrightarrow$ elimination rule. In other words, is a ND system that includes the substitution rule equivalent to the same ND system with the substitution rule replaced by the $\leftrightarrow$ elimination rule?
For example,
- A
- $A\leftrightarrow B$
- B (1,2,substitution rule)
can be rewritten as
- A
- $A\leftrightarrow B$
- $(A \to B) \land (B \to A)$ (2,$\leftrightarrow$ elimination)
- $A \to B$ (3, $\land$ E)
- B (1,4,MP)
There are also examples for sub-substitution. For example,
- $A\land B$
- $B\leftrightarrow C$
- $A\land C$ (1,2, substitution rule)
can be rewritten as
- $A\land B$
- $B\leftrightarrow C$
- B (1, $\land$ E)
- $(B \to C) \land (C \to B)$ (2,$\leftrightarrow$ elimination)
- $B \to C$ (4, $\land$ E)
- C (3,5, MP)
- A (1, $\land$ E)
- $A\land C$ (6,7, $\land$ I)
But I cannot replace the substitution rule with the $\leftrightarrow$ elimination rule for some sub-substitution, such as this one:
- $A\lor B$
- $B\leftrightarrow C$
- $A\lor C$ (1,2, substitution rule)
I wonder if the substitution rule is a derived rule or a basic rule that is absolutely necessary for a natural deduction system.
Note also that, this substitution rule is not the same as those in many logic books which select some tautologies of the form $A\leftrightarrow B$ such as $\lnot \lnot P\leftrightarrow P$ and $\lnot(P\lor Q)\leftrightarrow \lnot P\land\lnot Q$, then say A can be replaced by B in the following formulas(as the whole formula or a sub-formula); our substitution rule does not require $A\leftrightarrow B$ is a tautology . So, a related question is if the two types of substitution rule are equivalent?
Thanks.
Best Answer
There are a number of 'substitution principles' in logic, so I am glad you made clear exactly what you mean. In fact, let me make a few more distinctions, as those will be helpful once I get to the point of actually addressing your specific question.
OK, so first there is something that most texts will refer to as the Replacement Theorem. This can be seen as the 'Logical Equivalents Substitution Principle'. This principle is the meta-logical Theorem that states that if two statements $\phi$ and $\psi$ are logically equivalent, which we'll write as $\phi \Leftrightarrow \psi$, then if you have a statement that contains one or more instances of $\phi$ (let's call this statement $S(\phi)$ ), then if you replace any (some, or all) of those instances of $\phi$ with $\psi$, then the resulting statement $S(\psi)$ is logically equivalent to $S(\psi)$, i.e. $S(\phi) \Leftrightarrow S(\psi)$.
This principle is very close to what you describe at the end of the post, though one fundamental difference is that whereas the Replacement Theorem is a meta-logical theorem, you are describing what is known as a 'rule of equivalence': a formal inference rule that can be used in a formal proof system: they typically state that some equivalence can be 'applied' to a given statement in a proof, i.e. that given that $\phi \Leftrightarrow \psi$, we can replace any $\phi$ as it occurs in any given statement in a proof with $\psi$, and write down the resulting statement in our proof. You can find such rules in popular introductory logic textbooks by Copi, Hurley, and others, and note that their validity/soundness is guaranteed by the Replacement Theorem.
Aside from this fundamental difference between meta-theorem and formal inference rule, there are two other differences between the meta-logical Replacement Theorem and the typical 'equivalence rules' you find in such texts.
First, whereas the Replacement Theorem is about logical equivalence, an equivalence rule is a rule of inference, and thus reflects more a logical implication. Put differently, it would be more the counterpart of the meta-logical principle that is like the Replacement Theorem, but simply concludes that $S(\phi) \Rightarrow S(\psi)$. Of course, you can always go the other way around, but still: in a formal proof we are dealing with implication, not equivalence. It is when we 'do' boolean algebra to 'rewrite' one logic expression into some other logic expression that we are more dealing with equivalence ... and once again, the correctness of what we do when we do such a thing is guaranteed by the Replacement Theorem.
Second, as you point out, equivalence rules as part of a formal proof system typically point to a specific equivalence, like Double Negation, or DeMorgan. Indeed, each of some finite number of elementary equivalences is given its own equivalence rule that allows one to apply that equivalence to any (part of a) given statement in a formal proof and derive the result. In other words, formal proof systems do not have a general and single rule that reflects the general nature of the Replacement Theorem ...
... and there is a perfectly good reason for that! The whole idea of a formal proof is that it is a demonstration that breaks down that fact that something is a logical implication from something else into a series of elementary and 'obviously' valid implications. If we had a general rule that directly reflects the general nature of the Replacement Theorem, then we might as well have a rule that says: If a set of statement $\Gamma$ logically implies a statement $\psi$, then if in a proof you have statements $\Gamma$, then you can write down statement $\psi$ ... and now every formal proof would take exactly 1 step! This clearly violates the very idea behind a formal proof. Likewise, a formal rule that reflects the general Replacement Theorem is too powerful.
And there is another reason: Inference rules (whether they are rules of inference like Modus Tollens, or rules of equivalence like Double Negation) are supposed to be formal, i.e. they say "If you have a statement (or statements) that look like [this], then you can write down a statement that looks like [that]". As such, formal rules are supposed to be purely syntactical operations. A rule that would reflect the general Replacement Theorem would no longer be syntactical.
OK! With this as background, let's address your specific question(s). First: yes, we can totally define a formal inference rule (that we'll call $\leftrightarrow$ substitution) that says that if you have a statement $\phi \leftrightarrow \psi$, and you have a statement $\gamma$ that either is $\phi$ itself, or contains a number of instances of $\phi$, then the result of replacing any of all of those $\phi$'s with $\psi$'s in $\gamma$ is a statement you can now infer. Put schematically:
$1. \phi \leftrightarrow \psi$
$2. S(\phi)$
$3. S(\psi)$ ($1,2 \ \leftrightarrow$ substitution)
(with $S(\phi)$ and $S(\psi)$ as defined earlier in the post)
Now, as you correctly point out, this is not a rule of equivalence like you see in Copi, Hurley, etc. In this rule, $\phi$ and $\psi$ need not be logically equivalent. Rather, you simply have a material equivalence (or material biconditional) $\phi \equiv \psi$
In fact, as such one might wonder whether this is even a valid inference ... but it is. In fact, the meta-logical proof for the validity of this $\leftrightarrow$ substitution rule would be very similar to the proof of the Replacement Theorem.
I also want to point out that the rule is pretty handy to have. For example, the proofs in your post show how you can do certain derivations much more quickly using this $\leftrightarrow$ Substitution rule as opposed to having more traditional inference rules. Indeed, I personally do give my students this $\leftrightarrow$ Substitution rule as an 'advanced' rule of inference and tell them to go ahead and use it whenever they see fit.
Indeed, as a demonstration of the 'strength' of the $\leftrightarrow$ Substitution rule, please refer to this post where I make use of this rule in solving a puzzle of the well-known Knights and Knaves puzzle variety. ... Indeed, the rule is a great tool for solving any Knights and Knaves puzzle very quickly.
OK, so do books use it as part of their defined formal proof system? You say you have never seen it, and nor have I. I think one important reason is that it is really unlike any typical rule of inference or rule of equivalence .. it sort of sits in between. So I can totally see how people would not use it for aesthetical reasons.
Also, the rule is not necessary for a formal proof system to be complete: given that this rule reflects a valid inference, then any complete formal proof system (which is effectively any proof system you'll ever encounter in a text, since the author(s) will make darn sure it is complete!) can prove whatever you can derive using this rule.
This includes, by the way, the inference from $A \lor B$ and $B \leftrightarrow C$ to $A \lor C$ that you bring up as a last example. Of course! If we have a complete system, and given that the $\leftrightarrow$ Substitution rule reflects a sound inference, then that system should be able to do whatever you can achieve using $\leftrightarrow$ Substitution. For example, assuming some fairly common inference rules, including your:
$1. \phi \leftrightarrow \psi$
$2. (\phi \rightarrow \psi) \land (\psi \rightarrow \phi) \ (1, \ \leftrightarrow $ Elimination)
we can do:
$1. A \lor B$
$2. B \leftrightarrow C$
$3. (B \to C) \land (C \to B)$
$4. B \to C \ (3, \land E)$
$5. | A \ (Assume)$
$6. | A \lor C \ (5, \lor I)$
$7. | B \ (Assume)$
$8. | C \ (4,7 \ \to E)$
$9. | A \lor C \ (8, \lor I)$
$10. A \lor C \ (1, 4-5, 6-8, \lor E)$
Still, I wouldn't say that the $\leftrightarrow$ Substitution rule is a 'derived' inference rule in the sense that the typical rules you find in formal proof systems can proof this pattern ... exactly because it is an abstract pattern, i.e. exactly because it is neither the typical kind of rule of inference or rule of equivalence. What I mean is: In many proof systems, Modus Tollens is not an elementary rule of inference ... and yet I can provide a formal proof of that pattern (or at laast, I can use my other rules to show that $\{ P \to Q, \neg Q\} \vdash \neg P$). As such, Modus Tollens can be seen as a derived rule: once I have a proof of $\{ P \to Q, \neg Q\} \vdash \neg P$, I can 'box' it up, give it a name, and use it as a derived rule in future proofs. But I cannot do that for this $\leftrightarrow$ substitution rule, because of the abstract nature of the rule.
So, when you say:
I would say: no, the $\leftrightarrow$ Substitution rule is certainly not a basic rule that is necessary for a natural deduction system to be complete. But I would also say that: no, I would not call it exactly a 'derived rule' rule either. But: it is true that whatever you can do with the $\leftrightarrow$ Substitution rule (in an otherwise sound system) can also be proven in any other complete natural deduction system without that rule. (so if that is what you mean by 'derived', then sure, it is 'derived' in that sense).
Now, you also ask:
As you realize, it is not true that anything we can derive using just the $\leftrightarrow$ Elimination rule we can also derive using just the $\leftrightarrow$ Substitution rule. As the examples in your post, and also the proof above shows, we'll have to use other rules as well. As such, you correctly put this question of 'equivalence' in terms of whole proof systems.
Unfortunately, not knowing what those other rules are, we really cannot answer this question.
Sure, trivially, a sound and complete proof system that contains the $\leftrightarrow$ Elimination rule, but not the $\leftrightarrow$ Substitution rule will be equivalent to a sound and complete proof system that contains the $\leftrightarrow$ Substitution rule, but not the $\leftrightarrow$ Elimination rule. But that is not interesting, since the 'sound and complete' part does all the work.
A more interesting question is (and I am sure this is what you mean): if we have sound and complete proof system that contains the $\leftrightarrow$ Elimination rule, but not the $\leftrightarrow$ Substitution rule, can we swap out those two rules in the proof system, while still retaining soundness and completeness?
Here, the fact that the Substitution rule is so different in nature makes this difficult to answer. Normally when we ask such questions about the equivalence of proof systems when swapping out one rule with another, we simply show how you can emulate the one rule with the other, using any of the other rules of the proof system. And while this is what you do for some specific patterns in your post, this is of course not a proof that we can do this in general. Indeed, you already assumed that you had specific other rules to work with, and so did I in the proof above. But without such assumptions, answering this question becomes a good bit more difficult. Indeed, I am quite frankly a bit stumped how I would prove or disprove this claim.
Here are some things I can offer. First, let us suppose we don't use your $\leftrightarrow$ Elimination rule, but instead consider a more widely used version ... I'll call it $\leftrightarrow$ Elimination':
$1. \phi \leftrightarrow \psi$
$2. \phi$
$3. \psi \ (1, 2 \ \leftrightarrow $ Elimination')
Now, if we have a sound and complete system that has this rule as one of its rules, then it is clear that we can use the $\leftrightarrow $ Substition rule to emulate this rule, since it would be just a specific instance of it. So, replacing this $\leftrightarrow $ Elimination' rule with the $\leftrightarrow $ Substition rule retains completeness.
Also, in most proof systems that you will find in textbooks you can replace your original $\leftrightarrow $ Elimination rule with the $\leftrightarrow $ Substition rule, as you can most likely prove $(A \to A) \land (A \to A)$ without the use of the $\leftrightarrow $ Elimination rule, and thus you can do:
$1. A \leftrightarrow B$
$2. (A \to A) \land (A \to A)$
$3. (A \to B) \land (B \to A) \ (1, 2 \ \leftrightarrow $ Substitution)
But yeah, I don't quite know if this works for any sound and complete proof system: maybe the rules of the system are so intertwined that the proof of $(A \to A) \land (A \to A)$ would have to rely on the $\leftrightarrow $ Elimination rule? Unlikely, but I wonder if at least theoretically you could give a counterexample to the claim that we can simply swap out the $\leftrightarrow $ Elimination rule with the $\leftrightarrow $ Substitution rule.
Even worse, the abstract nature of the $\leftrightarrow $ Substitution rule makes it even harder to try and see how the other way around works: how you could swap out the $\leftrightarrow $ Substitution rule with the $\leftrightarrow $ Elimination rule (or even the $\leftrightarrow $ Elimination' rule) and retain completeness. If I ever get any furthe insights about this, I'll let you know.
These comments also apply to your last question as to whether or not you can swap out one or more rules of equivalence with the $\leftrightarrow $ Substitution rule and retain completeness ... and vice versa. Again, without knowing exactly what rules we are talking about, I am not sure how to prove or disprove this.