Tue 18 Jan 2022 13:55 - 14:20 at Salon III - Formalization of Logic, Algebra and Geometry Chair(s): Andrei Popescu

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.

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change