Session 3: Rules of Inference & Natural Deduction

Overview

Natural deduction: the rules, how to build a derivation tree, and how proofs are constructed forwards and backwards.

Lecturer

Ayman Kaçan

Session Information

• Date and Time: Monday 28 September 2026 — 17:30-19:30
• Place: (to be announced)
• Online Meeting Link
• Session Recording

Core Concepts

• Proof systems as syntactic games: ⊢ versus ⊨
• Inference rule notation: premises, conclusion, and side conditions
• Introduction and elimination rules for every connective (∧I/∧E, ∨I/∨E, →I/→E, ¬I/¬E, ⊥E)
• Derivation trees, built bottom-up and top-down
• Hypothetical reasoning and discharging assumptions
• Backward vs forward reasoning, with the same theorem proved both ways
• Soundness and completeness

Slides

Session 3 Slides: Download PDF

Readings

• Logic in Computer Science (Huth & Ryan), Ch. 1.2
• The Open Logic Project, Ch. 7, 8, 9, 10
• The Incredible Proof Machine — an interactive natural-deduction game

Exercises & Extra Steps

• Practice (not collected): derive ⊢ (p → q) → (¬q → ¬p)
• Practice (not collected): attempt ⊢ p ∨ ¬p using only intuitionistic rules and identify where it fails
• Problem Set 1 released today — due on paper at the start of S5 (Mon 21 Sep)

Navigation

• ← Previous: S2: Propositional Logic
• Back to Course Overview
• Next: S4: Predicate Logic — Quantifiers, Binding, Scope →

Questions? Reach out on the course WhatsApp!