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 — 18:00-19:30
• Place: Nicely 212
• Online Meeting Link
  • Meeting Number: 2398 637 3880
  • Password: BeK7KF3tm@6
• Session Recording
  • Password: KhmM8GK@

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

Slides

Session 3 Slides: Download PDF

Credit: The above slides were prepared by Ayman Kaçan.

Readings

• Logic in Computer Science (Huth & Ryan), Ch. 1.2
• Videos by Jad Abou Hawili on Natural Deduction Inferences Rules in Lean and Natural Deduction Proofs.
• The Open Logic Project, Ch. 10 (Sections 10.1, 10.2, 10.3, 10.4)
• 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!