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 provides a basic model for understanding the logical 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
A standard proof system based on introduction and elimination rules.
- Introduction and elimination rules
- Discharging assumptions
- Proof trees
Soundness and Completeness
Two theorems connecting provability with semantic validity. For first-order logic the two coincide (Gödel's completeness theorem).
- Soundness $\vdash \Rightarrow \models$
- Completeness $\models \Rightarrow \vdash$
- The bridges connecting syntax and semantics
Introduction to the λ-calculus
A fundamental formal 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 constructive proofs matter
Next step
Once you have grasped natural deduction and the λ-calculus, move on to the Intermediate level to study simple type theory and higher-order logic (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.