Definition:Natural Deduction System

Natural Deduction Systems

This page gathers together the various systems of natural deduction that can be found in various sources in the literature.

It may be taken for granted that this list is incomplete, and more or less arbitrary in what is and is not included.

The main factor driving inclusion or not is simply the specific sources directly available to whomever includes it.

Irving M. Copi: Symbolic Logic (4th Edition)

Source: Irving M. Copi: Symbolic Logic, 4th ed. (MacMillan, $1973$)

Rules of Inference

Modus Ponendo Ponens

\(\ds p\)

\(\implies\)

\(\ds q\)

\(\ds p\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds q\)

\(\)

\(\ds \)

Modus Tollendo Tollens

The Modus Tollendo Tollens can be symbolised by the sequent:

\(\ds p\)

\(\implies\)

\(\ds q\)

\(\ds \neg q\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds \neg p\)

\(\)

\(\ds \)

Hypothetical Syllogism

\(\ds p\)

\(\implies\)

\(\ds q\)

\(\ds q\)

\(\implies\)

\(\ds r\)

\(\ds \vdash \ \ \)

\(\ds p\)

\(\implies\)

\(\ds r\)

Disjunctive Syllogism

\(\ds p \lor q\)

\(\)

\(\ds \)

\(\ds \neg p\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds q\)

\(\)

\(\ds \)

Constructive Dilemma

\(\ds \paren {p \implies q} \land \paren {r \implies s}\)

\(\)

\(\ds \)

\(\ds p \lor r\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds q \lor s\)

\(\)

\(\ds \)

Destructive Dilemma

\(\ds \paren {p \implies q} \land \paren {r \implies s}\)

\(\)

\(\ds \)

\(\ds \neg q \lor \neg s\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds \neg p \lor \neg r\)

\(\)

\(\ds \)

Rule of Simplification

\(\ds p \land q\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds p\)

\(\)

\(\ds \)

Rule of Conjunction

\(\ds p\)

\(\)

\(\ds \)

\(\ds q\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds p \land q\)

\(\)

\(\ds \)

Rule of Addition

\(\ds p\)

\(\)

\(\ds \)

\(\ds \vdash \ \ \)

\(\ds p \lor q\)

\(\)

\(\ds \)

Rule of Replacement

Let the statements $P_1, P_2, \ldots, P_n$ be conclusions in a proof, on various assumptions.

Let $P_1, P_2, \ldots, P_n \vdash Q$ be a sequent for which we already have a proof.

Then we may infer, at any stage of a proof (citing SI), the conclusion $Q$ of the sequent already proved.

This conclusion depends upon the pool of assumptions upon which $P_1, P_2, \ldots, P_n$ rest.

The Rule of Replacement can then subsequently be used on the following:

De Morgan's Theorems: 1

$\vdash \paren {\neg p \lor \neg q} \iff \paren {\neg \paren {p \land q} }$

De Morgan's Theorems: 2

$\vdash \paren {\neg p \land \neg q} \iff \paren {\neg \paren {p \lor q} }$

Rule of Commutation: 1

$\vdash \paren {p \lor q} \iff \paren {q \lor p}$

Rule of Commutation: 2

$\vdash \paren {p \land q} \iff \paren {q \land p}$

Rule of Association: 1

$\vdash \paren {p \lor \paren {q \lor r} } \iff \paren {\paren {p \lor q} \lor r}$

Rule of Association: 2

$\vdash \paren {p \land \paren {q \land r} } \iff \paren {\paren {p \land q} \land r}$

Rule of Distribution: 1

$\vdash \paren {p \land \paren {q \lor r} } \iff \paren {\paren {p \land q} \lor \paren {p \land r} }$

Rule of Distribution: 2

$\vdash \paren {p \lor \paren {q \land r} } \iff \paren {\paren {p \lor q} \land \paren {p \lor r} }$

Double Negation

$\vdash p \iff \neg \neg p$

Transposition

$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$

Material Implication

$\vdash \paren {p \implies q} \iff \paren {\neg p \lor q}$

Material Equivalence: 1

$\vdash \paren {p \iff q} \iff \paren {\paren {p \implies q} \land \paren {q \implies p} }$

Material Equivalence: 2

$\vdash \paren {p \iff q} \iff \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} }$

Exportation

$\vdash \paren {\paren {p \land q} \implies r} \iff \paren {p \implies \paren {q \implies r} }$

Tautology: 1

$\vdash p \iff \paren {p \lor p}$

Tautology: 2

$\vdash p \iff \paren {p \land p}$