Natural deduction: swapping equivalent formulas or definitions

Question

In a natural deduction systems, I sometimes see what are called rules of replacement (also called rules of equivalence).

These include equivalences like DeMorgan's Laws, or contraposition. Take the latter as an example. I sometimes see the rule written like this:

$CP \,\colon \ (a \to b) \leftrightarrow (\lnot b \rightarrow \lnot a)$

Sometimes, I see it written with $::$ instead of $\leftrightarrow$, like this:

$CP\,\colon \ (a \rightarrow b) :: (\lnot b \rightarrow \lnot a)$

I take it that this equivalence has been proven already, and I take it that this rule is supposed to denote that, in a proof, any substitution instance of the formula that appears on one side of the $::$ symbol can be swapped with an equivalent substitution instance of the formula that appears on the other side of the $::$ symbol.

So, for example, I might have a proof that looks something like this:

$ \begin{matrix} \vdots & ~ & ~ \\ 5. & a \rightarrow b & 3, 4 ~ MP \\ \end{matrix} $

I can then use the CP rule to replace $a \rightarrow b$ with $\lnot b \rightarrow \lnot a$, like this:

$ \begin{matrix} \vdots & ~ & ~ \\ 5. & a \rightarrow b & 3, 4 ~ MP \\ 6. & \lnot b \rightarrow \lnot a & 5 ~ CP \\ \end{matrix} $

Two questions:

1. Is my understanding of this correct? If so, how exactly is this specified as an inference rule?
2. Can I use this technique for any other equivalence? For instance, say I have a theory with some axioms, and I prove some equivalence $\phi \leftrightarrow \psi$ specific to that theory. Can I then swap out either side of that equivalence in later proofs, much as happened in my pseudo-example with the CP rule? If so, how and when do I specify that as an inference rule (or rules)?

Another, related, question:

3. Suppose I stipulate a definition which does not extend the set of derivable theorems. For instance, perhaps I stipulate a definition that is notational syntactic sugar or something. Can I then freely swap in/out the definiens/defiendum in my proofs, similar to how it works with the CP pseudo-example?

Answer 1

In Natural Deduction we have no rules of replacement, but rules of inference.

We can introduce "derive rules", like e.g.:

$A \to B \vdash \lnot B \to \lnot A$

deriving them from basic rules:

1) $A \to B$ --- premise

2) $\lnot B$ --- assumed [a]

3) $A$ --- assumed [b]

4) $\bot$ --- contradiction from 3), 1) and 2)

5) $\lnot A$ --- from 3) and 4), discharging [b]

6) $\lnot B \to \lnot A$ --- from 2) and 5) by $\to$-intro, discharging [a].

Having done this, we can use the new rule in a derivation: it acts as an abbreviation for a sub-proof deriving the result from "basic" rules.

If the language has the bi-conditional connective, we have also the $↔$-elim rule:

from $A ↔ B$ infer $A \to B$ and $B \to A$,

that allows us to substitute equivalentes in a derivation.

---

Replacement is partially built-in into the system, through the schematic presentation of rules (the rules are expressed in the meta-language, with cariables $\varphi, \psi, \ldots$ that stay for formulas.

Then we can extend it with some sort of Substitution Theorem :

$\vdash (\varphi_1 ↔ \varphi_2) → (\psi [\varphi_1/p] ↔ \psi[\varphi_2/p])$.

Answer 2

Everything you propose here is certainly perfectly logically valid.

And, as such, everything can be made into a formal rule of inference.

However, if you have to provide a derivation using some specific formal proof system, it remains to be seen whether that system has actually formalized any of this. For example, some proof systems will have Contraposition is an actual rule of inference, while others may not.

But if you don't care too much about staying within the confines of some specific formal proof system, then again yes, go ahead and do everything you propose, since it is all perfectly valid from a semantical point of view.