lean4-logic
This project is aim to formalize some various results of mathematical logic in Lean Theorem Prover.
This book provides explanation and summaries of formalized concepts, theorems, propositions. Proofs of them are not explained, refer to the code or the references.
Full documentation is here.
Main Results
Classical Propositional Logic
- Soundness and completeness.
First-Order Logic
The list of main formalized results in first-order (Predicate) logics.
- Soundness and completeness.
- Gödel's First Incompleteness Theorem.
- Gödel's Second Incompleteness Theorem.
Superintuitionistic Propositional Logic
The list of main formalized results in superintuitionistic propositional logics.
- Soundness and completeness for Kripke semantics.
- Law of Excluded Middle doesn't hold in intuitionistic logic.
- Disjunctive property of intuitionistic logic.
Standard Modal Logic
The list of main formalized in standard modal logics.
- Definability of Kripke frame.
- Soundness and completeness for Kripke semantics.
- Gödel-McKensey-Tarski Theorem and Modal companion.
Import Graph
Generated by import-graph
Foundation
Arithmetization
Incompleteness
