Formalizing mathematical logic in Lean 4.
Main results of this repository. More detailed explanations are provided in Docs.
-
Logic: Fundamental notions shared by all logics (entailment, semantics, calculi, Lindenbaum algebras, …). -
Propositional: Propositional logic (classical and intuitionistic). -
FirstOrder: First-order logic- Completeness theorem
- Cut-elimination of first-order sequent calculus (Gentzen's Hauptsatz)
- Gödel–Gentzen negative translation
- Downward Löwenheim–Skolem theorem
- Intuitionistic first-order logic and Kripke semantics
-
Arithmetic: arithmetical theories (
$\mathsf{PA^-}$ ,$\mathsf{I}\Sigma_n$ ,$\mathsf{I\Delta_0 + \Omega_1}$ ,$\mathsf{R_0}$ ,$\mathsf{Q}$ , …), definability, exponentiation, hereditarily finite sets, and true arithmetic. -
Incompleteness
- Gödel's First and Second incompleteness theorems
- Gödel–Rosser's incompleteness theorem
- Löb's theorem
- Tarski's undefinability of truth
- Church's theorem and undecidability of first-order logic
-
Set theory:
$\mathsf{Z}$ ,$\mathsf{ZF}$ ,$\mathsf{ZFC}$ and their models.- Consistency of ZFC (relative to Lean's type theory)
- Downward Löwenheim–Skolem theorem for models of set theory
-
SecondOrder: Syntax, semantics, and derivations of second-order logic. -
Meta: Proof automation. -
Vorspiel: Supplemental definitions and theorems for Mathlib.
Results that depend on Foundation but are developed in their own repositories under the Formalized Formal Logic organization:
-
ProvabilityLogic: provability logics (
$\mathsf{GL}$ and its relatives), their Kripke semantics, and arithmetical completeness via the provability predicates formalized here.
See the organization page for the other repositories.
- Docs: catalogue of definitions and theorems, generated by doc-gen4.
- Catalogue: an overview of the formalized results across the organization.
Diagrams "Zoo" illustrate the Lean 4-verified interrelationships among theories.
They are generated from the environment by Zoo/ on every build; run just zoo to
regenerate them locally.
- A solid arrow
$\mathsf{A} \leftarrow \mathsf{B}$ indicates that$\mathsf{B}$ is strictly stronger than$\mathsf{A}$ ; that is,$\mathsf{B}$ is stronger than$\mathsf{A}$ , while$\mathsf{A}$ is not stronger than$\mathsf{B}$ , in terms of provability strength. - A dashed arrow
$\mathsf{A} \dashleftarrow \mathsf{B}$ indicates that$\mathsf{B}$ is stronger than$\mathsf{A}$ in terms of provability strength. - A double line
$\mathsf{A} \xlongequal{} \mathsf{B}$ indicates that$\mathsf{A}$ and$\mathsf{B}$ are equivalent in terms of provability strength.
See CONTRIBUTING.md for the contribution flow.
Foundation is a Lake project depending on Mathlib; the Lean version is pinned in lean-toolchain.
lake exe cache get # fetch prebuilt Mathlib oleans
lake buildList 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 Saitou, @iehality, ✉️:palalansouki@gmail.com)
- Overall design and maintenance.
- First-order logic.
- Intuitionistic first-order logic.
- Arithmetic, set theory, and incompleteness.
- Proof automation.
- Provability logic.
- SnO2WMaN (Mashu Noguchi, @SnO2WMaN, ✉️:me@sno2wman.net)
- Modal logic.
- Propositional logic (including intermediate logic).
- Provability logic.
- Interpretability logic.
- Miscellaneous repository maintenance (e.g. GitHub Actions).
This project is licensed under the Apache License 2.0.
If you wish to cite this repository in academic papers, refer to CITATION.cff.
Any financial support would be greatly appreciated. If you find this project valuable, please consider supporting us to sustain our OSS development.
We would like to thank the following backers.
Individuals and organizations that have supported us in the past.
- Proxima Technology (2024-2025)
- 随時 (@zuizi) (2025-10)