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:

  1. 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?
  • $\begingroup$ Regarding replacement, see e.g. the post proving-tautologically-equivalent. $\endgroup$ – Mauro ALLEGRANZA Mar 12 '18 at 14:59
  • $\begingroup$ Definitions have two kinds: def of "predicates" (they use the bi-conditional) and def of "terms" (they use the equality). For the first one: YES, the def allows us to replace in a context the definiens with the definiendum (and vice versa). $\endgroup$ – Mauro ALLEGRANZA Mar 12 '18 at 15:02
  • $\begingroup$ You can see the post are-if-and-iff-interchangeable-in-definitions for the formal treatment of definitional equivalences in FOL. $\endgroup$ – Mauro ALLEGRANZA Mar 12 '18 at 15:37
  • $\begingroup$ Thanks for the references. They are helpful. I'm trying to understand the the Tarski example in that last reference. Suppose I have an axiom that defines the $\leq$ predicate like this: $(x \leq y) \leftrightarrow \lnot (y > x)$. Suppose next that in a proof, on some line I derive $\lnot (y > x)$. On the next line, I want to replace that with $x \leq y$. What inference rule do I use to do that? Do I just cite the axiom? Or do I need to construct some other, derived rule? $\endgroup$ – user1439929 Mar 13 '18 at 2:35
  • $\begingroup$ If you have the "definitional" axiom $(x≤y) ↔ ¬(y>x)$ and you have derived $¬(y>x)$, you can use $↔$-elim [from $A ↔ B$ infer $A \to B$ (as well as $B \to A$)] to derive $¬(y>x) \to (x≤y)$ from the axiom and finally $(x≤y)$ by $\to$-elim. $\endgroup$ – Mauro ALLEGRANZA Mar 13 '18 at 7:01

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

  • $\begingroup$ Regarding replacement, when you say we can extend it with some sort of substitution theorem, is that something we'd do in the meta language? Or is that an inference rule? $\endgroup$ – user1439929 Mar 12 '18 at 17:32
  • $\begingroup$ @user1439929 - the proof of Subst Th is by induction: thus it is made in the meta-. $\endgroup$ – Mauro ALLEGRANZA Mar 12 '18 at 17:48
  • $\begingroup$ Is it possible to define a definitional axiom as a pair of inference rules. So, $A \leftrightarrow B$ would become $A / B$ and $B / A$? When I look at some of the examples in Negri and Plato's Proof Analysis book, it looks like they define axioms as inference rules. $\endgroup$ – user1439929 Mar 15 '18 at 12:21
  • $\begingroup$ @user1439929 - Yes; in ND axioms are introduction rules with $0$ premises $\endgroup$ – Mauro ALLEGRANZA Mar 15 '18 at 13:21

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.


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.