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

DOI10.1093/logcom/exaa073OpenAlexW3122736276MaRDI QIDQ5028312

Dominik Wehr, Dominik Kirst, Yannick Forster

Publication date: 8 February 2022

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exaa073

zbMATH Keywords

completenessfirst-order logicalgebraic semanticsKripke semanticstype theoryconstructive logicconstructive reverse mathematicsCoqdialogue semanticsTarksi semantics

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)

Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ Material dialogues for first-order logic in constructive type theory ⋮ \textsf{LOGIC}: a Coq library for logics ⋮ Unnamed Item

Uses Software

• Coq

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