Open AccessProving the consistency of Logic in Lean
Author(s) -
Luiz Carlos Rumbelperger Viana
Publication year - 2020
Language(s) - English
Resource type - Conference proceedings
DOI - 10.5753/wbl.2020.11452
Subject(s) - soundness , corollary , consistency (knowledge bases) , first order logic , semantics (computer science) , gas meter prover , computer science , automated theorem proving , calculus (dental) , programming language , mathematics , theoretical computer science , discrete mathematics , algebra over a field , pure mathematics , mathematical proof , medicine , geometry , dentistry
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.