Foundation
Formalizing mathematical logics in Lean 4.
Summary
Main Result in this repository. More results and details are in Book and Doc.
- Propositional Logic
- Tait-style calculus and completeness
- Completeness for Kripke semantics
- Disjunctive Property of intuitionistic logic
- Rejection Law of Excluded Middle in intuitionistic logic and sublogic relations
- First-Order Logic and Arithmetics
- Completeness Theorem
- Gödel-Gentzen Translation
- Cut-elimination of first-order sequent calculus (Gentzen's Hauptsatz)
- Arithmetic and Arithmetization
- Gödel's First and Second Incompleteness Theorems
- Basic Modal Logic (with modal operators
)
Documents
Sponsor
This project is supported by Proxima Technology.