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).
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
- Set theory: \mathsf{Z}, \mathsf{ZF}, \mathsf{ZFC} and their models.
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 (\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.
Documents
- Docs:
catalogue of definitions and theorems, generated by doc-gen4.
Zoo
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.
Arithmetic 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 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.