Negation rules in natural deduction

Question

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{equation}\begin{array}{c}{[\neg A]\\ \vdots\\ \bot}\end{array}\end{equation}}{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.

Answer 1

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

$$\dfrac{\begin{equation}\begin{array}{c}{[\neg A]\\ \vdots\\ \bot}\end{array}\end{equation}}{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{equation}\begin{array}{c}{[A]\\ \vdots\\ \bot}\end{array}\end{equation}}{\neg A}\neg I \quad = \quad \frac{\begin{equation}\begin{array}{c}{[A]\\ \vdots\\ \bot}\end{array}\end{equation}}{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\}$.