From 1931 until late in his life (at least 1970) Godel called for the pursuit of new axioms for mathematics to settle both undecided number-theoretical propositions (of the form obtained in his incompleteness results) and undecided set-theoretical propositions (in particular CH). As to the nature of these, Godel made a variety of suggestions, but most frequently he emphasized the route of introducing ever higher axioms of in nity. In particular, he speculated (in his 1946 Princeton remarks) that there might be (...) a uniform (though non-decidable) rationale for the choice of the latter. Despite the intense exploration of the \higher in nite" in the last 30-odd years, no single rationale of that character has emerged. Moreover, CH still remains undecided by such axioms, though they have been demonstrated to have many other interesting set-theoretical consequences. (shrink)

In this article, we discuss a simple argument that modal metaphysics is misconceived, and responses to it. Unlike Quine's, this argument begins with the observation that there are different candidate interpretations of the predicate ‘could have been the case’. This is analogous to the observation that there are different candidate interpretations of the predicate ‘is a member of’. The argument then infers that the search for metaphysical necessities is misguided in much the way the ‘set-theoretic pluralist’ claims that the search (...) for the true axioms of set theory is. We show that the obvious responses to this argument fail. However, a new response has emerged that purports to prove, from higher-order logical principles, that metaphysical possibility is the broadest kind of possibility applying to propositions, and is to that extent special. We distill two lines of reasoning from the literature, and argue that their import depends on premises that any ‘modal pluralist’ should deny. Both presuppose that there is a unique typed hierarchy, which is what the modal pluralist, in the context of higher-order logic, should disavow. In other words, both presupposes that there is a unique candidate for what higher-order claims could mean. We consider the worry that, in a higher-order setting, modal pluralism faces an insuperable problem of articulation, collapses into modal monism, is vulnerable to the Russell-Myhill paradox, or even contravenes the truism that there is a unique actual world, and argue that these worries are misplaced. We also sketch the bearing of the resulting ‘Higher-Order Pluralism’ on the theory of content. One theme of the discussion is that, if Higher-Order Pluralism is correct, then there is no fixed metatheory from which to characterize higher-order reality. (shrink)

Proof-theoretic reflection principles are schemas which attempt to express the soundness of arithmetical theories within their own language, e.g., ${\mathtt{{Prov}_{\mathsf {PA}} \rightarrow \varphi }}$ can be understood to assert that any statement provable in Peano arithmetic is true. It has been repeatedly suggested that justification for such principles follows directly from acceptance of an arithmetical theory $\mathsf {T}$ or indirectly in virtue of their derivability in certain truth-theoretic extensions thereof. This paper challenges this consensus by exploring relationships between reflection principles (...) and principles of mathematical and transfinite induction as well as the status of the latter with respect to various foundational characterizations of number theory. (shrink)

For several subsystems of second order arithmetic T we show that the proof-theoretic strength of T + (bar rule) can be characterized in terms of T + (bar induction) □ , where the latter scheme arises from the scheme of bar induction by restricting it to well-orderings with no parameters. In addition, we demonstrate that ACA + 0 , ACA 0 + (bar rule) and ACA 0 + (bar induction) □ prove the same Π 1 1 -sentences.

In [10] Friedman showed that is a conservative extension of <ε0for-sentences wherei= min, i.e.,i= 2, 3, 4 forn= 0, 1, 2 +m. Feferman [5], [7] and Tait [11], [12] reobtained this result forn= 0, 1 and even with instead of. Feferman and Sieg established in [9] the conservativeness of over <ε0for-sentences for alln. In each paper, different methods of proof have been used. In particular, Feferman and Sieg showed how to apply familiar proof-theoretical techniques by passing through languages with Skolem (...) functionals.In this paper we study the same choice principles in the presence of theBar Rule, which permits one to infer the scheme of transfinite induction on a primitive recursive relation ≺ when it has been proved that ≺ is wellfounded. The main result characterizes + as a conservative extension of a system of the autonomously iterated-comprehension axiom for-sentences. Forn= 0 this has been proved by Feferman in the form that + is a conservative extension of <Γ0; this was first done in [8] by use of the Gödel functional interpretation for the stronger systemZω+μ+ + and then more recently by the simpler methods of [9]. Jäger showed how the latter methods could also be used to obtain the general result of Theorem 1 below. (shrink)