<aside> 🎯

Comprehensive lecture notes covering the natural deduction proof system, including proof trees, inference rules for all logical operators, and worked examples demonstrating how to construct formal proofs.

</aside>

Topics covered:

• Natural deduction as a formal proof system
• Proof tree structure and notation
• Conjunction rules (introduction and elimination)
• Implication rules (introduction and elimination)
• Introducing and discharging assumptions
• Negation rules
• Disjunction rules
• Rules for falsity (⊥)
• Worked proof examples

What is Natural Deduction?

Natural deduction is a syntactic approach to formal proofs, based on the syntax of formulas.

<aside> 💡

Key idea: Natural deduction is a formal proof system where we construct proofs using inference rules that allow us to introduce or eliminate logical operators.

</aside>

Connection to Semantics

Because the natural deduction system is sound and complete:

• If we can prove something syntactically (⊢), it implies semantic entailment (⊨)
• A proof without any assumptions (⊢ φ) means the formula is a tautology