7. Metatheory and the Transition to Lean 4
Historical Materialist Hook
[RESEARCH REQUIRED: Map the absolute mathematical boundaries of formal systems. Utilize Alan Turing’s On Computable Numbers to establish the limits of mechanical computation and highlight its immediate weaponization in cryptographic warfare. Address the political economy of these limits with Don Lavoie’s Rivalry and Central Planning.]
Core Technical Synthesis
[RESEARCH REQUIRED: Establish the ultimate theoretical bridge between syntax and semantics by introducing Soundness and Completeness. Introduce Dependent Type Theory via the Lean 4 proof assistant. Explain how to view logical proofs as programs, authoring basic functional scripts where “tactics” serve as algorithmically verifiable mathematical proofs.]
Guided Example: Lean 4 Syntax
Proving a simple theorem in Lean:
theorem modus_ponens (P Q : Prop) (h1 : P → Q) (h2 : P) : Q :=
h1 h2Problem Set
Exercise 7.1
Draft a pseudo-code outline of a soundness proof. How does the structure of the syntax tree map onto the steps of the proof?
Dictionary Reference Map
- For metatheory (Soundness/Completeness): forall x Calgary (Magnus et al. 2025, 340-365)
- For introduction to Lean 4: Theorem Proving in Lean 4 (Avigad et al. 2024, 20-85)