Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coq (CPP 2022)

Sun 16 - Fri 28 January 2022 Philadelphia, Pennsylvania, United States

Who

Mark Koch, Dominik Kirst

Track

CPP 2022

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

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

Abstract

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.

Link to Preprint

https://www.ps.uni-saarland.de/Publications/documents/KochKirst_2022_Undecidability.pdf

Mark Koch

Saarland University

Dominik Kirst