Vtyjkyuk

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:

$
beginmatrix
vdots & ~ & ~ \
5. & a rightarrow b & 3, 4 ~ MP \
endmatrix
$

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

$
beginmatrix
vdots & ~ & ~ \
5. & a rightarrow b & 3, 4 ~ MP \
6. & lnot b rightarrow lnot a & 5 ~ CP \
endmatrix
$

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?

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])$.

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.