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 (, , , , , …), 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: , , and their models.
  - Consistency of ZFC (relative to Lean's type theory)
  - Downward Löwenheim–Skolem theorem for models of set theory
  - Set Theory Zoo
SecondOrder: Syntax, semantics, and derivations of second-order logic.
Meta: Proof automation.
Vorspiel: Supplemental definitions and theorems for Mathlib.

Further Results

Results that depend on Foundation but are developed in their own repositories under the Formalized Formal Logic organization:

ProvabilityLogic: provability logics ( and its relatives), their Kripke semantics, and arithmetical completeness via the provability predicates formalized here.

See the organization page for the other repositories.

Documents

Docs: catalogue of definitions and theorems, generated by doc-gen4.
Catalogue: an overview of the formalized results across the organization.

Zoo

Automatically generated¹ diagrams "Zoo" illustrate the Lean 4-verified interrelationships among theories and 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

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.

lake exe cache get   # fetch prebuilt Mathlib oleans
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 Saito, @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)

To reduce build time in GitHub Actions, generated in a separate repository, see Zoo. ↩