339 lines
13 KiB
Markdown
339 lines
13 KiB
Markdown
---
|
||
title: Natural Deduction
|
||
TARGET DECK: Obsidian::STEM
|
||
FILE TAGS: formal-system::natural-deduction
|
||
tags:
|
||
- logic
|
||
- natural-deduction
|
||
- programming
|
||
---
|
||
|
||
## Overview
|
||
|
||
Natural deduction is a proof system typically used alongside classical truth-functional [[prop-logic|propositional]] and [[pred-logic|predicate]] 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.
|
||
<!--ID: 1721655978485-->
|
||
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.
|
||
<!--ID: 1721655978490-->
|
||
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.
|
||
<!--ID: 1721655978493-->
|
||
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.
|
||
<!--ID: 1721655978499-->
|
||
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.
|
||
<!--ID: 1721655978506-->
|
||
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.
|
||
<!--ID: 1721825479315-->
|
||
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.
|
||
<!--ID: 1721825479325-->
|
||
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.
|
||
<!--ID: 1721825479330-->
|
||
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.
|
||
<!--ID: 1721825479336-->
|
||
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.
|
||
<!--ID: 1721656449679-->
|
||
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.
|
||
<!--ID: 1721656449704-->
|
||
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.
|
||
<!--ID: 1721655978513-->
|
||
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.
|
||
<!--ID: 1721655978517-->
|
||
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.
|
||
<!--ID: 1721656730330-->
|
||
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.
|
||
<!--ID: 1721656601607-->
|
||
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.
|
||
<!--ID: 1721656416280-->
|
||
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.
|
||
<!--ID: 1721656416284-->
|
||
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.
|
||
<!--ID: 1721656416288-->
|
||
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.
|
||
<!--ID: 1721656416291-->
|
||
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.
|
||
<!--ID: 1721656730337-->
|
||
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.
|
||
<!--ID: 1721656601613-->
|
||
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.
|
||
<!--ID: 1721665510225-->
|
||
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.
|
||
<!--ID: 1721785548092-->
|
||
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.
|
||
<!--ID: 1721665541946-->
|
||
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.
|
||
<!--ID: 1721665541949-->
|
||
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.
|
||
<!--ID: 1721665541951-->
|
||
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.
|
||
<!--ID: 1721665510228-->
|
||
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.
|
||
<!--ID: 1721665541955-->
|
||
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.
|
||
<!--ID: 1721666244354-->
|
||
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.
|
||
<!--ID: 1721666244357-->
|
||
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.
|
||
<!--ID: 1721666244359-->
|
||
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.
|
||
<!--ID: 1721666244361-->
|
||
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.
|
||
<!--ID: 1721666244362-->
|
||
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.
|
||
<!--ID: 1721666244367-->
|
||
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.
|
||
<!--ID: 1721666244366-->
|
||
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.
|
||
<!--ID: 1721666244364-->
|
||
END%%
|
||
|
||
## Bibliography
|
||
|
||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|