Definition:Natural Deduction System/Copi

This page has been identified as a candidate for refactoring of medium complexity. In particular: Some of the rules cited need to be made more precise: currently some of them are dual rules, each of which need to be separated Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Definition

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

Sources

• 1973: Irving M. Copi: Symbolic Logic (4th ed.) ... (previous) ... (next): $3$: The Method of Deduction: $3.1$: Formal Proof of Validity