Foundation

Formalizing mathematical logic in Lean 4.

Structure & Summary

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).
  • Completeness of Tait calculus
• 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.
    • Arithmetic Theory Zoo
  • 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
• ProvabilityLogic: Provability logic
  • Arithmetical completeness theorems of \mathsf{GL} and \mathsf{S}, \mathsf{Grz}, and \mathsf{GL} + \Box^n \bot
  • Classification of provability logics
  • Provability Logic Zoo
• SecondOrder: Syntax, semantics, and derivations of second-order logic.
• Syntax: Syntax shared by first-order and second-order logic.
• Meta: Proof automation.
• Vorspiel: Supplemental definitions and theorems for Mathlib.

Documents

• Docs: catalogue of definitions and theorems, generated by doc-gen4.

Zoo

Diagrams “Zoo” illustrate the Lean 4-verified interrelationships among theories and logics. They are generated by Zoo/; 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.

Arithmetic Theory Zoo

Provability Logic Zoo

Contributing

See CONTRIBUTING.md for the contribution flow.

Building

Foundation is a Lake project depending on Mathlib; the Lean version is pinned in lean-toolchain. It requires elan and just.

just cache
lake build

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 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).

License

This project is licensed under the Apache License 2.0.

Citation

If you wish to cite this repository in academic papers, refer to CITATION.cff.

Financial Supports

Any financial support would be greatly appreciated. If you find this project valuable, please consider supporting us to sustain our OSS development.

Open Collective

We would like to thank the following backers.

Previous Backers

Individuals and organizations that have supported us in the past.

• Proxima Technology (2024-2025)
• 随時 (@zuizi) (2025-10)