Proving the consistency of Logic in Lean | Zendy

Luiz Carlos Rumbelperger Viana | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Proving 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 , calculus (dental) , automated theorem proving , programming language , sequential consistency , mathematics , higher order logic , discrete mathematics , theoretical computer science , algebra over a field , description logic , pure mathematics , mathematical proof , consistency model , medicine , geometry , dentistry , correctness

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research