notebook/notes/formal-system/proof-system/natural-deduction.md

13 KiB

title TARGET DECK FILE TAGS tags
Natural Deduction Obsidian::STEM formal-system::natural-deduction
logic
natural-deduction
programming

Overview

Natural deduction is a proof system typically used alongside classical truth-functional prop-logic and pred-logic logic. It is meant to mimic the patterns of reasoning that one might "naturally" make when forming arguments in plain English.

%%ANKI Basic Why is natural deduction named the way it is? Back: It is mean to mimic the patterns of reasoning one might "naturally" make when forming arguments in plain English. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Axioms

Natural deduction is interesting in that it has no axioms.

%%ANKI Basic How many axioms does natural deduction include? Back: 0 Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Inference Rules

Scoped to propositional logic, there are 10 inference rules corresponding to an "introduction" and "elimination" of each propositional logic operator.

%%ANKI Basic With respect to propositional logic, how many inference rules does natural deduction include? Back: 10 Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How are natural deduction's inference rules categorized into two? Back: As introduction and elimination rules. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic With respect to propositional logic, how are natural deduction's inference rules categorized into five? Back: As an introduction and elimination rule per propositional logic operator. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Negation

For propositions E_1 and E_2, \neg{\text{-}}I{:} \quad \begin{array}{c} \text{from } E_1 \text{ infer } E_2 \land \neg E_2 \ \hline \neg E_1 \end{array} and \neg{\text{-}}E{:} \quad \begin{array}{c} \text{from } \neg E_1 \text{ infer } E_2 \land \neg E_2 \ \hline E_1 \end{array}

%%ANKI Basic In natural deduction, how is negation introduction denoted? Back: As \neg{\text{-}}I. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In natural deduction, how is negation elimination denoted? Back: As \neg{\text{-}}E. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \neg{\text{-}}I expressed in schematic notation? Back: \begin{array}{c} \text{from } E_1 \text{ infer } E_2 \land \neg E_2 \ \hline \neg E_1 \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \neg{\text{-}}E expressed in schematic notation? Back: \begin{array}{c} \text{from } \neg E_1 \text{ infer } E_2 \land \neg E_2 \ \hline E_1 \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Conjunction

For propositions E_1, \ldots, E_n, \land{\text{-}}I{:} \quad \begin{array}{c} E_1, \ldots, E_n \ \hline E_1 \land \cdots \land E_n \end{array} and \land{\text{-}}E{:} \quad \begin{array}{c} E_1 \land \cdots \land E_n \ \hline E_i \end{array}

%%ANKI Basic In natural deduction, how is conjunction introduction denoted? Back: As \land{\text{-}}I. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In natural deduction, how is conjunction elimination denoted? Back: As \land{\text{-}}E. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \land{\text{-}}I expressed in schematic notation? Back: \begin{array}{c} E_1, \ldots, E_n \ \hline E_1 \land \cdots \land E_n \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \land{\text{-}}E expressed in schematic notation? Back: \begin{array}{c} E_1 \land \cdots \land E_n \ \hline E_i \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \ 2. & Q \ 3. & R \ \hline & P \land R \end{array} Back: \land{\text{-}}I Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \land Q \ \hline & P \end{array} Back: \land{\text{-}}E Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Disjunction

For propositions E_1, \ldots, E_n, \lor{\text{-}}I{:} \quad \begin{array}{c} E_i \ \hline E_1 \lor \cdots \lor E_n \end{array} and \lor{\text{-}}E{:} \quad \begin{array}{c} E_1 \lor \cdots \lor E_n, E_1 \Rightarrow E, \ldots, E_n \Rightarrow E \ \hline E \end{array}

%%ANKI Basic In natural deduction, how is disjunction introduction denoted? Back: As \lor{\text{-}}I. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In natural deduction, how is disjunction elimination denoted? Back: As \lor{\text{-}}E. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \lor{\text{-}}I expressed in schematic notation? Back: \begin{array}{c} E_i \ \hline E_1 \lor \cdots \lor E_n \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \lor{\text{-}}E expressed in schematic notation? Back: \begin{array}{c} E_1 \lor \cdots \lor E_n, E_1 \Rightarrow E, \ldots, E_n \Rightarrow E \ \hline E \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \ 2. & Q \ \hline & R \lor P \end{array} Back: \lor{\text{-}}I Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \lor Q \ 2. & P \Rightarrow R \ 3. & Q \Rightarrow R \ \hline & P \end{array} Back: \lor{\text{-}}E Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Implication

For propositions E_1, \ldots, E_n, {\Rightarrow}{\text{-}}I: \quad \begin{array}{c} \text{from } E_1, \cdots, E_n \text{ infer } E \ \hline (E_1 \land \cdots \land E_n) \Rightarrow E \end{array} and {\Rightarrow}{\text{-}}E: \quad \begin{array}{c} E_1 \Rightarrow E_2, E_1 \ \hline E_2 \end{array}

%%ANKI Basic In natural deduction, how is implication introduction denoted? Back: As {\Rightarrow}{\text{-}}I. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is {\Rightarrow}{\text{-}}I expressed in schematic notation? Back: \begin{array}{c} \text{from } E_1, \cdots, E_n \text{ infer } E \ \hline (E_1 \land \cdots \land E_n) \Rightarrow E \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In natural deduction, how is implication elimination denoted? Back: As {\Rightarrow}{\text{-}}E. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Modus ponens is associated with which propositional logic operator? Back: \Rightarrow Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Does modus ponens correspond to an introduction or elimination rule? Back: Elimination. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is {\Rightarrow}{\text{-}}E expressed in schematic notation? Back: \begin{array}{c} E_1 \Rightarrow E_2, E_1 \ \hline E_2 \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is modus ponens expressed in schematic notation? Back: \begin{array}{c} E_1 \Rightarrow E_2, E_1 \ \hline E_2 \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \Rightarrow Q \ 2. & P \ \hline & R \end{array} Back: N/A. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \Rightarrow Q \ 2. & P \ \hline & Q \end{array} Back: {\Rightarrow}{\text{-}}E Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Biconditional

For propositions E_1 and E_2, {\Leftrightarrow}{\text{-}}I: \quad \begin{array}{c} E_1 \Rightarrow E_2, E_2 \Rightarrow E_1 \ \hline E_1 \Leftrightarrow E_2 \end{array} and {\Leftrightarrow}{\text{-}}E: \quad \begin{array}{c} E_1 \Leftrightarrow E_2 \ \hline E_1 \Rightarrow E_2, E_2 \Rightarrow E_1 \end{array}

%%ANKI Basic In natural deduction, how is biconditional introduction denoted? Back: As {\Leftrightarrow}{\text{-}}I. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In natural deduction, how is biconditional elimination denoted? Back: As {\Leftrightarrow}{\text{-}}E. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is {\Leftrightarrow}{\text{-}}I expressed in schematic notation? Back: \begin{array}{c} E_1 \Rightarrow E_2, E_2 \Rightarrow E_1 \ \hline E_1 \Leftrightarrow E_2 \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \Rightarrow Q \ 2. & Q \Rightarrow P \ \hline & Q \Leftrightarrow P \end{array} Back: {\Leftrightarrow}{\text{-}}I Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is {\Leftrightarrow}{\text{-}}E expressed in schematic notation? Back: \begin{array}{c} E_1 \Leftrightarrow E_2 \ \hline E_1 \Rightarrow E_2, E_2 \Rightarrow E_1 \end{array} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which natural deduction inference rule is used in the following? \begin{array}{rc} 1. & P \Leftrightarrow Q \ \hline & Q \Rightarrow P \end{array} Back: {\Leftrightarrow}{\text{-}}E Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Bibliography

  • Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.