Proving the consistency of Logic in Lean
Luiz Carlos Rumbelperger Viana · 2020
We implement classical first-order logic with equality in the Lean Interactive Theorem Prover (ITP), and prove its soundness relative to the usual semantics. As a corollary, we prove the consistency of the calculus.