4.1 Natural deduction: rules and proof construction

Natural deduction is a way of reasoning in logic using rules for introducing and eliminating logical connectives. It's like building with Lego blocks, where each block is a logical statement and the rules tell you how to connect them.

In this section, we'll learn about the specific rules for different logical operators like "and," "or," and "if-then." We'll also see how to use these rules to construct proofs, which are step-by-step arguments that show a conclusion follows from given premises.

Introduction and Elimination Rules

Conjunction Rules

• Conjunction introduction rule ($\wedge$I) allows inferring a conjunction ($A \wedge B$) if both conjuncts ($A$ and $B$) have been derived separately
• Conjunction elimination rules ($\wedge$E) allow inferring either conjunct ($A$ or $B$) from a conjunction ($A \wedge B$)
• Left conjunction elimination ($\wedge$E1) infers the left conjunct ($A$) from a conjunction ($A \wedge B$)
• Right conjunction elimination ($\wedge$E2) infers the right conjunct ($B$) from a conjunction ($A \wedge B$)

Disjunction Rules

• Disjunction introduction rules ($\vee$I) allow inferring a disjunction ($A \vee B$) if either disjunct ($A$ or $B$) has been derived
• Left disjunction introduction ($\vee$I1) infers a disjunction ($A \vee B$) from the left disjunct ($A$)
• Right disjunction introduction ($\vee$I2) infers a disjunction ($A \vee B$) from the right disjunct ($B$)
• Disjunction elimination rule ($\vee$E) allows inferring a formula ($C$) from a disjunction ($A \vee B$) if $C$ can be derived from each disjunct ($A$ and $B$) separately

Implication and Negation Rules

• Implication introduction rule ($\rightarrow$I) allows inferring an implication ($A \rightarrow B$) if the consequent ($B$) can be derived assuming the antecedent ($A$)
• Implication elimination rule ($\rightarrow$E), also known as modus ponens, allows inferring the consequent ($B$) from an implication ($A \rightarrow B$) and its antecedent ($A$)
• Negation introduction rule ($\neg$I), also known as reductio ad absurdum, allows inferring the negation of an assumption ($\neg A$) if a contradiction can be derived from that assumption
• Negation elimination rule ($\neg$E), also known as ex falso quodlibet, allows inferring any formula ($B$) from a contradiction ($A \wedge \neg A$)

Quantifiers and Hypothetical Reasoning

Quantifier Rules

• Universal quantifier introduction rule ($\forall$I) allows inferring a universally quantified formula ($\forall x A(x)$) if $A(c)$ has been derived for an arbitrary constant $c$
• Universal quantifier elimination rule ($\forall$E) allows inferring an instance ($A(t)$) of a universally quantified formula ($\forall x A(x)$) for any term $t$
• Existential quantifier introduction rule ($\exists$I) allows inferring an existentially quantified formula ($\exists x A(x)$) from an instance ($A(t)$) for some term $t$
• Existential quantifier elimination rule ($\exists$E) allows inferring a formula ($C$) from an existentially quantified formula ($\exists x A(x)$) if $C$ can be derived assuming $A(c)$ for a new constant $c$

Hypothetical Reasoning and Assumptions

• Hypothetical reasoning involves making assumptions and deriving conclusions from those assumptions
• Assumptions are temporary premises used in the course of a proof
• Discharge of assumptions occurs when the assumption is no longer needed and can be removed from the proof
• Discharging an assumption often corresponds to the application of an introduction rule ($\rightarrow$I, $\neg$I, $\forall$I, $\exists$E)

Proof Representation

Proof Trees

• Proof trees are graphical representations of proofs in natural deduction
• Nodes in a proof tree represent formulas, and edges represent the application of inference rules
• The root of the tree is the conclusion of the proof, and the leaves are the assumptions or axioms
• Proof trees provide a clear and intuitive way to visualize the structure of a proof

Fitch-style Notation

• Fitch-style notation is a linear representation of proofs in natural deduction
• Proofs are written as a sequence of lines, with each line containing a formula and the justification for that formula
• Assumptions are indicated by vertical bars (|) that scope over the lines that depend on the assumption
• Fitch-style notation is more compact than proof trees and is often used in practice