-/- 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)

In this paper we study the interpretations of a weak arithmetic, like Buss’s theory $\mathsf{S}^{1}_{2}$, in a given theory $U$. We call these interpretations the arithmetics of $U$. We develop the basics of the structure of the arithmetics of $U$. We study the provability logic of $U$ from the standpoint of the framework of the arithmetics of $U$. Finally, we provide a deeper study of the arithmetics of a finitely axiomatized sequential theory.

De Rijke introduced a unary interpretability logic $$\textbf{il}$$, and proved that $$\textbf{il}$$ is the unary counterpart of the binary interpretability logic $$\textbf{IL}$$. In this paper, we find the unary counterparts of the sublogics of $$\textbf{IL}$$.

We present a quite simple proof of the fixed point theorem for GL. We also use this proof to show that Sambin's algorithm yields a fixed point.