The Logic and Metaphysics Workshop will meet on February 10th from 2:00-4:00 in-person at the Graduate Center (Room 7395) for a talk by Sergei Artemov (CUNY).

Title: Consistency of PA is a serial property, and it is provable in PA

Abstract: We revisit the question of whether the consistency of Peano Arithmetic PA can be established in PA and answer it affirmatively. Since PA-derivations are finite objects, their Gödel codes are standard natural numbers, and PA-consistency is equivalent to the series ConS(PA) of arithmetical formulas “n is not a code of a proof of 0 = 1” for numerals n = 0, 1, 2, … In contrast, in the consistency formula Con(PA) “for all x, x is not a proof of 0 = 1,” the quantifier “for all x” captures standard and nonstandard numbers, Con(PA) is strictly stronger than PA-consistency. Adopting Con(PA) as PA-consistency was a strengthening fallacy: the unprovability of Con(PA) does not yield the unprovability of PA-consistency. A proof of a serial property is a selector proof: prove that each instance has a proof. We selector prove ConS(PA) thus showing that PA-consistency is provable in PA. We discuss other theories and perspectives for Hilbert’s consistency program.