Mathematical Logic: Basic
Building proof systems
About this level
At the Basic level we actually build proof systems. Natural deduction gives each logical connective an "introduction rule" and an "elimination rule," and this is precisely the propositional layer of a proof-checking kernel. We then study how the assembled proof system meshes with semantics (soundness and completeness), the λ-calculus as a model of computation, and the decisive fork for constructive mathematics: intuitionistic vs. classical logic (whether to accept the law of excluded middle).
Prerequisites
- Introduction (the syntax/semantics distinction, the idea of inference rules)
- Basics of functions and mappings
Contents
Natural Deduction
The standard form of a proof system.
- Introduction and elimination rules
- Discharging assumptions
- Proof trees
Soundness and Completeness
Provable ⟺ true.
- Soundness $\vdash \Rightarrow \models$
- Completeness $\models \Rightarrow \vdash$
- The bridges connecting syntax and semantics
Introduction to the λ-calculus
The minimal model of computation.
- Untyped λ-calculus and β-reduction
- Simply typed λ-calculus
- Terms and types
Intuitionistic vs. Classical Logic
On the law of excluded middle.
- Excluded middle $A \lor \neg A$
- What a constructive proof is
- Why sangi insists on being constructive
Next step
Once you have grasped natural deduction and the λ-calculus, move on to the Intermediate level to study simple type theory (HOL), the sequent calculus and cut elimination, strong normalization, and the basis of proof assistants with the LCF architecture. Intuitionistic logic also connects to the existing article Constructive Proof.