A rigorous, constructive exposition and formalization of first-order logic, Peano Arithmetic, and metamathematics within the framework of Homotopy Type Theory (HoTT).
This work develops formal deductive systems from the ground up as type-theoretic environments. It constructs well-formed terms, formulas, capture-avoiding substitution, and derivation trees as syntactic inductive types. The exposition culminates in the arithmetization of syntax and proof verification via Gödel numbering, demonstrating that logical proofs function as decidable mathematical relations.
- Formal Syntax & ASTs: Inductive definitions of terms, formulas, variable binding, and capture-avoiding substitution.
- Proof Theory & Deductive Systems: Formalization of derivation trees and inference rules for Peano Arithmetic.
- Arithmetization (Gödel Numbering): Unique prime-factorization encodings of syntax trees, finite sequences, and proof derivations into ℕ.
- Decidable Metamathematics: Constructive proofs establishing the decidability of syntactic identity and proof verification.
-
Constructive Foundations: Built strictly within Homotopy Type Theory, leveraging path induction, identity types,
$\Sigma$ -types, and$\Pi$ -types.