2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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\}$.

$\endgroup$
9
  • $\begingroup$ 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? $\endgroup$ – Gergely Nov 3 '20 at 13:57
  • $\begingroup$ 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. $\endgroup$ – lemontree Nov 3 '20 at 14:12
  • $\begingroup$ 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." $\endgroup$ – lemontree Nov 3 '20 at 14:18
  • $\begingroup$ OK but how A comes into the picture then? $\endgroup$ – Gergely Nov 3 '20 at 14:32
  • 1
    $\begingroup$ 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$. $\endgroup$ – lemontree Nov 3 '20 at 14:56

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.