Proving the consistency of Logic in Lean
Resumo
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.
Palavras-chave:
Proof assistants, Lean, Intuitionistic Type Theory, First Order Logic
Referências
From, A. H., Jensen, A. B., Schlichtkrull, A., and Villadsen, J. (2020). Teaching a formalized logical calculus. Electronic Proceedings in Theoretical Computer Science, 313:73–92.
Han, J. M. and van Doorn, F. (2019). A formalization of forcing and the unprovability of the continuum hypothesis.
Jeremy Avigad, R. Y. L. and van Doorn, F. (2017). Logic and Proof. https://leanprover.github.io/logic_and_proof/ [accessed 4/29/2020].
Martin-Löf, P. (1982). Constructive mathematics and computer programming. Amsterdam: North- Holland Publishing Company.
Viana, L. C. R. (2020). Github repo: https://github.com/maxd13/logic-soundness.git.revision: f15dfd4.
Han, J. M. and van Doorn, F. (2019). A formalization of forcing and the unprovability of the continuum hypothesis.
Jeremy Avigad, R. Y. L. and van Doorn, F. (2017). Logic and Proof. https://leanprover.github.io/logic_and_proof/ [accessed 4/29/2020].
Martin-Löf, P. (1982). Constructive mathematics and computer programming. Amsterdam: North- Holland Publishing Company.
Viana, L. C. R. (2020). Github repo: https://github.com/maxd13/logic-soundness.git.revision: f15dfd4.
Publicado
26/08/2020
Como Citar
VIANA, Luiz Carlos Rumbelperger.
Proving the consistency of Logic in Lean. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 1. , 2020, Evento Online.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2020
.
p. 1-8.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2020.11452.
