On Notions of Provability

Abstract

In this thesis, we study notions of provability, i.e. formulas B(x,y) such that a formula ' is provable in T if, and only if, there is m 2 N such that T ` B(p'q,m) (m plays the role of a parameter); the usual notion of provability, k-step provability (also known as k-provability), s-symbols provability are examples of notions of provability. We develop general results concerning notions of provability, but we also study in detail concrete notions. We present partial results concerning the decidability of k- provability for Peano Arithmetic (PA), and we study important problems concerning k-provability, such as Kreisel’s Conjecture and Montagna’s Problem: (8n 2 N.T `k steps '(n)) =) T ` 8x.'(x), [Kreisel’s Conjecture] Does PA `k steps PrPA(p'q) ! ' imply PA `k steps '? [Montagna’s Problem] Incompleteness, Undefinability of Truth, and Recursion are di↵erent entities that share important features; we study this in detail and we trace these entities to common results. We present numeral forms of completeness and consistency, numeral completeness and numeral consistency, respectively; numeral completeness guarantees that, whenever a⌃b1(S12)-formula'(x~)issuchthatQ~x~.'(x~)istrue(whereQ~ isanyarrayofquantifiers), then this very fact can be proved inside S12, more precisely S12 ` Q~ x~.Pr⌧(p'(x~• )q). We examine these two results from a mathematical point of view by presenting the minimal conditions to state them and by finding consequences of them, and from a philosophical point of view by relating them to Hilbert’s Program. The derivability condition “provability implies provable provability” is one of the main derivability conditions used to derive the Second Incompleteness Theorem and is known to be very sensitive to the underlying theory one has at hand. We create a weak theory G2 to study this condition; this is a theory for the complexity class FLINSPACE. We also relate properties of G2 to equality between computational classes.