An Introduction to Natural Deduction
summary
Natural deduction gets taught by walking through exact rules, writing and collapsing concrete proofs, then encoding them as programs so you can check they actually hold. Workshop shows a Haskell verifier library that accepts tree-structured derivations, returns errors or a sequent, and can generate LaTeX source for typeset proofs. Exercises produce explicit proofs (conjunction, implication, disjunction, negation) and their Haskell inhabitants, illustrating the Curry–Howard correspondence. The verifier runs and flags mistakes with readable messages.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:20Natural Deduction
- 5:25Natural Deduction Rules
- 6:24Example Proof
- 9:42Exercise
- 19:40Elimination
- 28:45Disjunction
- 29:24Conjunction
- 35:47Truth and Falsity
- 37:20Negation
- 47:07Cancellation
- 47:53How did I decide to negate
- 48:56Taking a break
- 49:29Rule for elimination
- 54:31Proof checker
- 57:15Curry Howard correspondence
related talks
26m(...) How to turn (Liquid) Haskell into a theorem prover
41mWar Time Proofs and Futuristic Programs
11mWhat are Dependent Types
01h 00mIntroduction to Coq - Part 1 of 2
35mProof Theory Impressionism: Blurring the Curry-Howard Line
10mWhen Does a Program Typecheck?
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
01h 46mWrite Some Idris