Foundation

Formalizing mathematical logic in Lean 4.

Structure & Summary

Main results of this repository. More detailed explanations are provided in the Catalogue and Docs.

• Propositional: Propositional Logic
  • Tait-style Calculus and Completeness
  • Completeness for Kripke semantics
  • Disjunctive Property of intuitionistic logic
  • Propositional Logic Zoo
• FirstOrder: First-Order Logic
  • Completeness Theorem
  • Cut-Elimination of First-Order Sequent Calculus (Gentzen's Hauptsatz)
  • Gödel-Gentzen Translation
  • Arithmetic
    • Gödel's First and Second Incompleteness Theorems
    • Arithmetic Theory Zoo
  • Set Theory
    • Consistency of ZFC
    • Set Theory Zoo
• Modal: Basic Modal Logic (with modal operators )
  • Kripke Semantics
  • Neighborhood Semantics
  • Gödel-McKinsey-Tarski Theorem and Modal Companions
  • Boxdot Conjecture
  • Modal Logic Zoo
• ProvabilityLogic: Provability Logic
  • Solovay's Arithmetical Completeness Theorem for GL
• InterpretabilityLogic: Interpretability Logic
  • Veltman Semantics
  • Interpretability Logic Zoo
• Meta: Proof automation.
• Logic: Fundamental tools for various logics.
• Vospiel: Supplemental definitions and theorems for mathlib.

Documents

• Catalogue, summary of results, generated by [verso].
• Docs, catelogue of definitions and theorems, generated by doc-gen4.
• Zoo, diagram of interrelationships among proof systems.

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

Set Theory Zoo

Propositional Logic Zoo

Modal Logic Zoo

Interpretability Logic Zoo

Contributing

For instructions on how to build the project, run tests, and contribute, see CONTRIBUTING.

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.
  • Interpretability 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 for us. If you found this project valuable, to sustain our OSS development, please consider support us.

Open Collective

We would like to thanks the following backers.

Previous Backers

Individuals and organizations that have supported us in the past.

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