13 KiB
| title | TARGET DECK | FILE TAGS | tags | |||
|---|---|---|---|---|---|---|
| Natural Deduction | Obsidian::STEM | formal-system::natural-deduction |
|
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 With respect to propositional logic, how are natural deduction's inference rules divided into two categories? 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 divided into five categories? 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 & R \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.