Consistency and Provability Workshop

The Consistency and Provability workshop will take place on Monday, April 27, in room 302 at the Institute of Computer Science, Neubrückstrasse 10, 3rd floor.

Schedule

Abstracts

Hilbert's consistency program was largely abandoned in the 1930s when Gödel Second Incompleteness Theorem, G2, was interpreted as yielding the paradigmatic Unprovability of Consistency Thesis, UCT: “There exists no consistency proof of a system that can be formalized in the system itself” (Encyclopaedia Britannica).

We show that the Gödelian model was a non-equivalent redefinition of Hilbert's original, serial definition of consistency. We offer a proof of Hilbert's consistency of Peano Arithmetic PA, formalizable in PA. This renders the UCT false in its “naïve” form and removes the perceived logical barrier to self-verifying AI and Automated Theorem Proving.

By distinguishing between the Gödelian model (essential for comparing the strength of theories) and the Hilbertian model (designed for internal self-verification), we propose a balanced foundational landscape. This shift allows autonomous reasoning systems to move from a paradigm of blind trust to one of rigorous, internal formal verification.

The slides are available here.

The notion of selector proof was introduced by Artemov as part of his analysis of consistency and the formalisation of metamathematics. Contrary to the case with "standard" provability, theories can selector prove their own consistency.

We will explore various technical results concerning selector proofs and show how they interact with traditional proof-theoretic notions such as relative consistency, proof-theoretic ordinals, and provably-recursive functions. Along the way, a characterisation of the selector-provable formulas of Peano Arithmetic will be provided.

Japaridze's polymodal logic, also known as GLP, is one of the most famous and studied provability logics. It arises, for example, by interpreting the n-th modality as a provability in Peano's Arithmetic with all true Pi_n-sentences. However, its semantics are far from trivial, as it is not Kripke complete. Thus, it has been common to prove the arithmetical completeness of GLP via studying some fragment of it that has Kripke complete semantics.

We propose a new way of studying GLP through proof theory, by providing the first (non-nested) sequent calculus for it and showing its analycity syntactically. Then we use this sequent calculus to provide a new arithmetical completeness proof (through Solovay's method) that works directly in GLP.

This is joint work with Thomas Studer.