Negation rules in natural deduction

There are various treatments of using negation in natural deduction for classical logic.

Let me quote bits of it:

$$\frac{}{\top}\top I$$

$$\frac{\bot}{A}\bot E\quad ex\ falso\ quodlibet$$

$$\frac{A\rightarrow\bot}{\neg A}\neg I$$

$$\frac{}{A\vee \neg A}tertium\ non\ datur$$

$$\frac{A\quad \neg A}{\bot}law\ of\ contradiction$$

$$\frac{A}{\neg\neg A}double\ negation\ 1$$

$$\frac{\neg\neg A}{A}double\ negation\ 2$$

$$\frac{$$\begin{array}{c}{[\neg A]\\ \vdots\\ \bot}\end{array}$$}{A}indirect\ proof$$

What is a standard way of building this, what are the axioms and how are the other rules are proved?

You might answer this by referring to some reference.

The only true "negation rule" needed is reductio ad absurdum aka proof by contradiction:

$$\dfrac{$$\begin{array}{c}{[\neg A]\\ \vdots\\ \bot}\end{array}$$}{A}\bot$$

It is important to note that RAA is not an instance of negation introduction (see below) but actually a separate rule.

$$\neg A$$ can be defined as syntactic sugar for what is actually $$A \to \bot$$, and $$\top$$ as $$\neg \bot$$ and hence $$\bot \to \bot$$. There is no deduction rule needed for switching between the two, they are treated as literally same formula that just looks different:

$$\neg A \quad = \quad A \to \bot$$ $$\top \quad = \quad\neg \bot \quad = \quad \bot \to \bot$$

Negation introduction and elimination is then a special case of implication introduction and elimination (negation elimination is what you call law of contradiction, and implication elimination is also known as modus ponens):

$$\frac{$$$$\begin{array}{c}{[A]\\ \vdots\\ \bot}\end{array}$$$$}{\neg A}\neg I \quad = \quad \frac{$$$$\begin{array}{c}{[A]\\ \vdots\\ \bot}\end{array}$$$$}{A \to \bot}\to I$$



$$\frac{A\quad \neg A}{\bot}\neg E \quad = \quad \frac{A\quad A \to \bot}{\bot}\to E$$ EFQL is just RAA with no assumption discharged (see the comments for a discussion on the difference between the two):

$$\frac{\bot}{A}\text{EFQL} \quad \rightsquigarrow \quad \frac{\bot}{A}\bot$$

The other rules can then be derived from these primitive rules:

For double negation,

$$\dfrac{A}{\neg\neg A}\neg \neg I \quad \rightsquigarrow \quad \dfrac{\dfrac{[\neg A]^1 \quad A}{\bot}\neg E}{\neg \neg A}\neg I^1 \quad = \quad \dfrac{\dfrac{[A \to \bot]^1 \quad A}{\bot}\to E}{(A \to \bot) \to \bot}\to I^1$$

and

$$\dfrac{\neg \neg A}{A}\neg \neg E \quad \rightsquigarrow \quad \dfrac{\dfrac{\neg \neg A \quad [\neg A]^1}{\bot}\neg E}{A}\bot^1 \quad = \quad \dfrac{\dfrac{(A \to \bot) \to \bot \quad [A \to \bot]^1}{\bot}\to E}{A}\bot^1$$

For the axioms,

$$\dfrac{}{\top}\top I \quad = \quad \dfrac{}{\neg \bot}\top I \quad \rightsquigarrow \quad \dfrac{[\bot]^1}{\neg \bot}\neg I \quad = \quad \dfrac{[\bot]^1}{\bot \to \bot}\to I^1$$

and finally, $$\dfrac{}{A\vee \neg A}\text{TND} \quad \rightsquigarrow \quad$$

see here; their $$(* B)$$ is our $$* E$$ (eliminiation) and $$(* E)$$ is $$* I$$ (introduction).

So natural deduction doesn't need axiom as primitives: Everything can be derived from the basic set of inference rules $$\{\land I, \land E, \lor I, \lor E, \to I, \to E, \bot\}$$.

• Thanks indeed. The only thing I cannot grasp is how I imagined Reduction ad Absurdum as Ex Falso Quodlibet. Could you elaborate or give a reference? Nov 3, 2020 at 13:57
• For rules that allow to discharge assumptions, it is allowed to not actually discharge all occurrences of the assumption, and even to not have the assumption present in the derivation at all. RAA would allow us to discharge assumptions of the form $\neg A$ that led to $\bot$, but we are also allowed to use the rule if we do not have such an assumption. This application then coincides with EFQL. Nov 3, 2020 at 14:12
• See e.g. D. van Dalen Logic and Structure p. 34: "W.r.t. the cancellation of hypotheses, we note that one does not necessarily cancel all occurrences of such a proposition \psi. [...] Furthermore, one may apply (-> I) [and RAA] if there is no hypothesis available for cancellation." Nov 3, 2020 at 14:18
• OK but how A comes into the picture then? Nov 3, 2020 at 14:32
• It's the conclusion we'd also get if we had the assumption $\neg A$. Since we could have started off with any negative formula except we don't need it, the conclusion can be an arbitrary formula $A$. Nov 3, 2020 at 14:56