Foundation
Formalizing mathematical logic in Lean 4.
Structure & Summary
Main results of this repository. More detailed explanations are provided in the Book and Doc.
FirstOrder
: First-Order Logic and Arithmetics- Completeness Theorem
- Cut-elimination of first-order sequent calculus (Gentzen's Hauptsatz)
- Arithmetic
- Gödel's First and Second Incompleteness Theorems
- Arithmetic Theory Zoo
IntFO
: Intuitionistic First-Order LogicModal
: Basic Modal Logic (with modal operators) Propositional
: Propositional LogicProvabilityLogic
: Provability LogicMeta
: Proof automation.Logic
: Fundamental tools for various logics.Vospiel
: Supplemental definitions and theorems for mathlib.
Documents
Zoo
Automatically generated diagrams "Zoo", illustrate the Lean4-verified interrelationships among proof systems.
- A solid arrow
indicates that is strictly stronger than ; that is, is stronger than , while is not stronger than , in terms of provability strength. - A dashed arrow
indicates that is stronger than in terms of provability strength. - A double line
indicates that and are equivalent in terms of provability strength.
Arithmetic Theory Zoo
Modal Logic Zoo
Propositional Logic Zoo
Developers
List of contact information and areas of expertise of the current main developers. If you have any interest or questions, create a new issue or contact us directly.
- Palalansoukî (Shogo Saito, @iehality, ✉️:palalansouki@gmail.com)
- Overall design and maintenance.
- First-order logic.
- Intuitionistic first-order logic.
- Proof automation.
- Provability logic.
- SnO2WMaN (Mashu Noguchi, @SnO2WMaN, ✉️:me@sno2wman.net)
- Modal logic.
- Propositional logic (including intermediate logic).
- Provability logic.
- Miscellaneous repository maintenance (e.g. GitHub Actions)
If you with to cite this repository in academic papers, refer to CITATION.cff.
Financial Supports
Any financial supports would be grateful. If you considered, please contact us.
Previous Sponsors
Companies and organizations that have supported us in the past.
- Proxima Technology (2024-2025)