Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, October 4, 2021 - 3:30pm

Sergei Artemov

CUNY Graduate Center


University of Pennsylvania

via Zoom

Link available upon request

We argue that there is a class of widely used and readily formalizable arithmetical proofs of universal properties which are not accounted for in the traditional unprovability of consistency analysis. On this basis, we offer a mathematical proof of consistency for Peano Arithmetic PA and demonstrate that this proof is formalizable in PA. This refutes the wide spread belief that there exists no consistency proof of a system that can be formalized in the system itself. Gödel’s Second Incompleteness theorem yields that PA cannot derive the consistency formula ConPA. This does not interfere with our formalized proof of PA-consistency which is not a derivation of the consistency formula ConPA.