The idea of provability logic arose in the seventies in work of G. Boolos, R. Solovay, and others, as an attempt to explore certain “modal effects” in the metamathematics of the first order arithmetic. Namely, the formal provability predicate Prτ(x), originally constructed by Gödel, has several properties resembling the necessity operator of common modal logics: the Löb’s derivability conditions,
look just like an axiomatization of a subsystem of S4:
We may form “arithmetical semantics” for formulas in the propositional modal language as follows: we substitute arithmetical sentences for propositional atoms, Prτ for boxes, and we ask whether the resulting sentence (the “arithmetical realization” or “provability interpretation” of the modal formula) is provable in our arithmetic T. The provability logic then consists of modal formulas, which are “valid” in every such “model”.
Solovay showed that this simple provability logic (known as GL) has a nice axiomatization, Kripke-style semantics and decision procedure. Moreover it is very stable: almost all reasonable theories T yield the same logic.
Further investigation concentrated on generalization of the Solovay’s result. In one direction, we may ask about the provability logic for theories which are not covered by the “almost all” above. This concerns e.g. theories based on the intuitionistic logic, such as HA, HA + MP + ECT0 etc., and weak classical theories, such as IΔ0 + Ω1 or even S21.
The second direction is to change the meaning of the modal operator. We may replace Prτ with some more pathological provability predicate (e.g. the “Rosser’s provability predicate”, which enables T to prove its own consistency), provability predicates for non-r.e. theories (such as the second order arithmetic with the ω-rule), “validity in all transitive models” in strong enough set theories and so on. More importantly, we may use a binary modal connective expressing relative interpretability over the base theory, or a similar binary relation (Π01-conservativity, local interpretability, Σ01-interpolability, “tolerance” etc.).
Finally, we may take two (or more) theories into account. The simplest way is to keep the modal language with one operator, translated as the provability predicate for the first theory, T, and form a logic consisting of modal formulas, such that all their arithmetical realizations are provable in the second theory, S. (A remarkable special case is S = Th(ℕ), the “true arithmetic”, which leads to the so-called absolute provability logic of T.) These logics were completely classified for any reasonable choice of T and S, due to S. Artëmov, L. Beklemishev and others.
Another way (perhaps more natural) is to use a bimodal language, with two separate necessity operators (say, □ and △) corresponding to provability predicates for both of the theories, Prτ and Prσ. Such a bimodal logic (denoted by PRL(T,S)) is capable of expressing basic relationship between T and S, e.g. certain reflection principles, partial conservativity or axiomatization properties (such as finite or bounded complexity axiomatizability of one theory over the other). No general characterizations of possible bimodal logics are known, in fact only a few of them were described so far, mostly for natural pairs of subsystems of PA. The first known was the bimodal logic for locally essentially reflexive pairs of sound theories (e.g. PRL(PA,ZF) or PRL(IΣ1,PA)), given by T. Carlson (see [Car86]), five other systems are due to L. Beklemishev ([Bek94] and [Bek96])—typical situations where they are applicable include PRL(IΣk,IΣℓ), PRL(IΔ0 + EXP,PRA), PRL(PA,PA + Con(ZF)), PRL(PA,PA + {Conn(PA); n∈ω}), PRL(ZFC,ZFC + CH). (Here Conn(T) is the iterated consistency assertion for T: Con1(T) = Con(T), Conn+1(T) = Con(T + Conn(T)).)
The formation of a bimodal provability logic needs both theories to be formulated in one and the same language (usually, but not necessarily, the language of the arithmetic). If we use theories with different languages, such as in the example PRL(PA,ZF) above, it is tacitly assumed that there is a fixed natural interpretation of the first theory in the second one (e.g. the standard model of PA in ZF), and we treat the second theory as the set of all sentences of the language of the first theory, which are provable in the second theory under this interpretation (i.e. the arithmetical sentences provable in ZF about ω, in our example). Alternatively, we may identify the first theory with the set of its axioms interpreted in the language of the second theory.
In this thesis, we will study an extension of the bimodal provability logic, designed for the situation of two particular theories with two different languages. We will distinguish between the two languages even at the modal level, and perhaps most importantly, we will deal with two different interpretations of the first theory in the second one. Thus our modal language will contain:
(One would expect that there were two sort-switching operators, one for each interpretation. However this would decrease significantly the readability of the resulting modal formulas, and anyway four non-boolean connectives is a lot, therefore we decided not to include the second sort-switching operator into our modal language. Instead, we allow formulas of the first sort to act directly as formulas of the second sort, i.e. the second operator is “invisible”. No ambiguity arises, because the context always determines uniquely the sort of a formula.)
Our two theories are Peano arithmetic (PA) and the Alternative Set Theory (AST) of P. Vopěnka (axiomatized by A. Sochor). There were several reasons for this choice:
The material is organized as follows. Chapter 1 deals with the Alternative Set Theory. The goal of this chapter is to present everything about AST that we will need for the treatment of our provability logic. We do not expect AST to be a “common knowledge”, hence we have included a detailed description of its axioms. Then we give some elementary facts provable in AST and we introduce a bit of the model theory of the classical first-order logic in AST (because the derivation of the most important modal principle we use depends on a construction of saturated models within AST). We do not go into details in this chapter, we just briefly sketch some basic steps with references to the (hopefully original) sources. A self-contained presentation would be possible, but it would be too long for our purposes and it would lead us far away from the main subject of this thesis (which is the provability logic), anyway only a small piece of chapter 1 is new here (this small piece is given with full proof, of course).
Chapter 2 investigates the provability logic. In section 2.1 we define our extension of the bimodal language and its intended “arithmetical” semantics, and we present an axiomatization of our provability logic and two auxiliary systems. Section 2.2 starts with the definition of a variant of the Kripke semantics suitable for our purposes, then we prove that the two auxiliary systems are complete w.r.t. their Kripke semantics. In section 2.3 we prove the arithmetical completeness of the provability logic, using the Kripke completeness results of section 2.2. As the proof is rather complicated, we have broken part of it into separate lemmas. We end this section with some examples, and we also put here several random facts that we considered worth mentioning, without a detailed discussion. In particular, we include here a short description of some interesting subsystems of our provability logic, which use the ordinary bimodal language and are therefore comparable to the above mentioned bimodal provability logics of L. Beklemishev and T. Carlson.