Mathematical Logic: Introduction
The gateway to syntax, semantics, proof, and Curry–Howard
About this level
The introduction builds the most basic viewpoint of mathematical logic. The key idea is to distinguish "manipulating symbols (syntax)" from "what they mean (semantics)." Once you can draw this distinction, you can recast the everyday word "proof" in formal terms, and you reach the doorway to the Curry–Howard world, where "a proof is also a program."
Prerequisites
- High-school mathematics
- Familiarity with logical words such as "implies," "and," "for all"
- It helps to have read Proof: Logical Operations and Quantifiers
Contents
Formal Systems: Syntax and Semantics
The starting point of all logic.
- Syntax as symbol manipulation
- Semantics as truth and models
- $\vdash$ (derivable) and $\models$ (true)
Propositional Logic via Inference Rules
The simplest logic.
- Connectives $\land, \lor, \to, \neg$
- The idea of inference rules
- Relation to truth tables
Predicate Logic and Quantifiers
"For all" and "there exists."
- Predicates and variables
- Universal $\forall$, existential $\exists$
- Bound and free variables
What a Proof Is, Formally
Making the everyday word precise.
- Proof as a derivation (a sequence of rule applications)
- Axioms and inference rules
- The idea of proof checking
A Gentle Introduction to Curry–Howard
A bird's-eye view of the field's backbone.
- Propositions = types
- Proofs = programs
- Proof reduction = computation
Next step
Once you have grasped the syntax/semantics distinction and the Curry–Howard idea, move on to the Basic level to actually build proof systems via natural deduction (introduction and elimination rules), and study soundness and completeness, the λ-calculus, and intuitionistic vs. classical logic.
What you can understand at this level
Separating syntax and semantics
Understand the central distinction that "arranging symbols by the rules" and "being correct (true)" are two different things.
Systems of inference rules
See logic not as "truth tables" but as a system of "what can be derived from which rules."
Proofs and programs coincide
Grasp the intuition of the Curry–Howard correspondence, bridging to the later chapters on type theory and proof assistants.