Publication details

Saarland University Computer Science

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               

Login to edit

Legal notice, Privacy policy