The Provability of Consistency

Sergei Artemov

Published 2019-02-20Version 1

Provability semantics suggests well-principled notions of constructive truth and constructive falsity of classical sentences in Peano arithmetic PA. F is constructively true iff PA proves F. F is constructively false iff PA proves that for each x, there is a proof that x is not a proof of F. We also consider an associated notion of constructive consistency of PA, CCon(PA), for each x, there is a proof that x is not a proof of 0=1. We show that PA proves CCon(PA) hence there is no a Goedel-style impossibility barrier for case-by-case consistency proofs. Furthermore, we prove a finitary version of constructive consistency directly, for any PA-derivation S we find a finitary proof that S does not contain 0=1. This proves consistency of PA by finitary means and appears to vindicate Hilbert program of establishing consistency of formal theories.