Logic Workshop

December 4
Sergei Artemov, CUNY
Provability of Consistency: A New Foundational Landscape

The informal Brouwer-Heyting-Kolmogorov (BHK) semantics maps classical formulas to their constructive readings. Later frameworks, such as Martin-Löf's Intuitionistic Type Theory, bypassed the classical language to construct intuitionistic analogs directly: formulas and proofs gave way to dependent types and terms. This became the language of Automated Theorem Proving (ATP), but created the illusion that the constructive domain was insulated from the classical one. Conceived by Gödel in the 1930's and developed in the 1990's, the Logic of Proofs made BHK semantics rigorous, thus bridging the classical and constructive domains. In this framework, the constructive semantics of $\forall xF(x)$ is a selector proof: a pair consisting of a function $s(x)$ (the selector) and a verification that, for all $x$, $s(x)$ is a proof of $F(x)$.

This construct also decisively contributes to classical foundations. Selector proofs are accepted in everyday mathematics, are conservative over Peano Arithmetic (PA), and can be used safely in PA reasoning without extending the pool of its theorems. With this tool, we build a mathematical proof of PA-consistency formalizable in PA, thus refuting the paradigm that consistency is unprovable within a theory. This creates a new foundational landscape with impacts on Automated Theorem Proving and AI.