Lean4 Logic Formalization
Usage
Contributing
References and Related Works
Preliminaries
Definitions and Notations
Computability
Classical Logics
Classical Propositional Logic
1. Syntax and Semantics
First-Order Logic
Non-Classical Logics
Superintuitionistic Propositional Logic
Standard Modal Logic

Logic Formalization in Lean 4

Usage

Add following to lakefile.lean.

require logic from git "https://github.com/FormalizedFormalLogic/Foundation"