Lean4 Logic Formalization
1.
Usage
2.
Contributing
3.
References and Related Works
Preliminaries
4.
Definitions and Notations
5.
Computability
Classical Logics
6.
Classical Propositional Logic
6.1.
Syntax and Semantics
7.
First-Order Logic
7.1.
Term and Formula
7.1.1.
Binder Notation
7.2.
Deduction System
7.3.
Semantics
7.4.
Completeness
7.5.
Arithmetics
7.5.1.
Theories of Arithmetics
7.5.2.
Theory IΣ₀
7.5.3.
Theory IΣ₁
7.5.4.
Gödel's First Incompleteness Theorem
7.5.5.
Gödel's Second Incompleteness Theorem
7.6.
Interpretation
Non-Classical Logics
8.
Superintuitionistic Propositional Logic
8.1.
Axioms
8.2.
Deduction
8.2.1.
Glivenko's Theorem
8.3.
Kripke Semantics
8.3.1.
Soundness
8.3.2.
Completeness
8.4.
Rejection Law of Excluded Middle
8.5.
Disjunctive Property
9.
Standard Modal Logic
9.1.
Axioms
9.2.
Deduction
9.3.
Kripke Semantics
9.3.1.
Soundness
9.3.2.
Completeness
9.4.
On GL
9.4.1.
Frame Definability
9.5.
Strengh between Logics
9.6.
Undefinability of Frame Property
9.7.
Modal Companion
Light
Rust
Coal
Navy
Ayu
Logic Formalization in Lean 4
Completeness for Kripke Semantics
Standard completeness proof using canonical models, etc.
instance : Complete 𝐈𝐧𝐭 𝔽(Ax(𝐈𝐧𝐭))