Completeness theorems for first-order logic analysed in constructive type theory

DOI10.1007/978-3-030-36755-8_4zbMath1485.03248arXiv2006.04399OpenAlexW2995956541MaRDI QIDQ2177578

Dominik Wehr, Yannick Forster, Dominik Kirst

Publication date: 6 May 2020

Full work available at URL: https://arxiv.org/abs/2006.04399

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Metamathematics of constructive systems (03F50) Type theory (03B38)

Related Items (4)

Trakhtenbrot’s Theorem in Coq ⋮ Constructive and mechanised meta-theory of intuitionistic epistemic logic ⋮ Material dialogues for first-order logic in constructive type theory ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: Completeness theorems for first-order logic analysed in constructive type theory