Conceptions of Absolute Provability

In the philosophical portion of this dissertation, I develop an account of absolute provability as this notion was understood by Gödel, Post, Tarski, and other twentieth century logicians. In Chapter 1, I consider some problems facing existing accounts of absolute provability, accounts which describe this notion as involving an idealization from concrete mathematical practice. I propose an alternative "top-down" approach to absolute provability, on which we devise a proof concept satisfying certain essential properties of proof. I describe two such properties: the subgroundedness requirement, the requirement that one should not adopt as absolute a method of proof P which admits extensions by further methods that can be seen to be correct on the same basis as P; and the axiom of solvability, the axiom that all definite mathematical propositions can either be proved, refuted, or proved to be undecidable. In Chapter 2, I describe and contrast Post and Gödel's respective conceptions of absolute provability. I argue that the common features of their conceptions reflect a shared adherence to the subgroundedness requirement as an essential property of proof. In Chapter 3, I describe another family of conceptions of absolute provability which includes the conceptions of Cohen, Mostowski, and Hamkins. On these "limitative" accounts, absolute provability serves to close research problems which can be compellingly argued to be absolutely undecidable. The inclination to settle problems in this way, I argue, reflects an implicit adherence to the axiom of solvability. In Chapter 4, I develop a formal framework for representing a proof-concept satisfying the two essential properties described in chapter one. I use this framework to argue that absolute provability is in a certain sense ineffable, but that it is nevertheless amenable to study by formal methods. In the mathematical part of the dissertation, I define and study the provability logics associated with Woodin's notions of Ω-consequence and Ω-provability. I demonstrate that most of these logics contain GL, and I give upper and lower bounds for a number of such logics. In particular, in a certain metatheory W, the provability logic of Ω-consequence from W is precisely GL.