-/- Provability logic is a modal logic that is used to investigate what arithmetical theories can express in a restricted language about their provability predicates. The logic has been inspired by developments in meta-mathematics such as Gödel’s incompleteness theorems of 1931 and Löb’s theorem of 1953. As a modal logic, provability logic has been studied since the early seventies, and has had important applications in the foundations of mathematics. -/- From a philosophical point of view, provability logic is interesting because (...) the concept of provability in a fixed theory of arithmetic has a unique and non-problematic meaning, other than concepts like necessity and knowledge studied in modal and epistemic logic. Furthermore, provability logic provides tools to study the notion of self-reference. (shrink)

Provability logics are modal or polymodal systems designed for modeling the behavior of Gödel’s provability predicate and its natural extensions. If Λ is any ordinal, the Gödel-Löb calculus GLPΛ contains one modality [λ] for each λ < Λ, representing provability predicates of increasing strength. GLPω has no non-trivial Kripke frames, but it is sound and complete for its topological semantics, as was shown by Icard for the variable-free fragment and more recently by Beklemishev and Gabelaia for the full logic. In (...) this paper we generalize Beklemishev and Gabelaia’s result to GLPΛ for countable Λ. We also introduce provability ambiances, which are topological models where valuations of formulas are restricted. With this we show completeness of GLPΛ for the class of provability ambiances based on Icard polytopologies. (shrink)

Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of GLP. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.

Ordinal functions may be iterated transfinitely in a natural way by taking pointwise limits at limit stages. However, this has disadvantages, especially when working in the class of normal functions, as pointwise limits do not preserve normality. To this end we present an alternative method to assign to each normal function f a family of normal functions Hyp[f]=〈fξ〉ξ∈OnHyp[f]=〈fξ〉ξ∈On, called its hyperation, in such a way that f0=idf0=id, f1=ff1=f and fα+β=fα∘fβfα+β=fα∘fβ for all α, β.Hyperations are a refinement of the Veblen hierarchy (...) of f. Moreover, if f is normal and has a well-behaved left-inverse g called a left adjoint, then g can be assigned a cohyperationcoH[g]=〈gξ〉ξ∈OncoH[g]=〈gξ〉ξ∈On, which is a family of initial functions such that gξgξ is a left adjoint to fξfξ for all ξ. (shrink)

We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment (...) of GLP Λ. (shrink)

Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”.For a set of formulas Γ, define predicative oracle reflection for T over Γ ) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then$$\forall \,\lambda (...) < {\rm{\Lambda }}\,.$$In particular, define predicative oracle consistency ) as Pred–O–RFN{0=1}.Our main result is as follows. Let ATR0 be the second-order theory of Arithmetical Transfinite Recursion, ${\rm{RCA}}_0^{\rm{*}}$ be Weakened Recursive Comprehension and ACA be Arithmetical Comprehension with Full Induction. Then,$${\rm{ATR}}_0 \equiv {\rm{RCA}}_0^{\rm{*}} + {\rm{Pred - O - Cons\ }}\left \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - Cons\ }}\left \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - RFN}}\,_{{\bf{\Pi }}_2^1 } \left.$$We may even replace ${\rm{RCA}}_0^{\rm{*}}$ by the weaker ECA0, the second-order analogue of Elementary Arithmetic.Thus we characterize ATR0, a theory often considered to embody Predicative Reductionism, in terms of strong reflection and consistency principles. (shrink)