Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq

Mark Koch; Dominik Kirst

Publication details

Programming Systems

Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq

Mark Koch, Dominik Kirst

Certified Programs and Proofs (CPP), January 17-18, 2022, Philadelphia, Pennsylvania, U.S.A., ACM, 2022

We mechanise central metatheoretic results about second-order logic (SOL) using the Coq proof assistant. Concretely, we consider undecidability via many-one reduction from Diophantine equations (Hilbert's tenth problem), incompleteness regarding full semantics via categoricity of second-order Peano arithmetic, and completeness regarding Henkin semantics via translation to mono-sorted first-order logic (FOL). Moreover, this translation is used to transport further characteristic properties of FOL to SOL, namely the compactness and Löwenheim-Skolem theorems.

Project page

Download PDF Show BibTeX

@CONFERENCE{KochKirst:2022:Undecidability,
  title = {Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq},
  author = {Mark Koch and Dominik Kirst},
  year = {2022},
  publisher = {ACM},
  booktitle = {Certified Programs and Proofs (CPP), January 17-18, 2022, Philadelphia, Pennsylvania, U.S.A.},
}

Legal notice, Privacy policy