Consistency and Provability Workshop

The Consistency and Provability workshop will take place on Monday, April 27, in the afternoon at the University of Bern. The exact time and location is to be announced.

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 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.