Emil Jeřábek

Master’s thesis, Faculty of Philosophy and Arts, Charles University, Prague, 2001, 44 pp. [PS, PDF] [BIB]

Master’s thesis, Faculty of Philosophy and Arts, Charles University, Prague, 2001, 44 pp. [PS, PDF] [BIB]

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* + *ECT*_{0}
etc., and weak classical theories,
such as *I*Δ_{0} + Ω_{1}
or even *S*_{2}^{1}.

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 (Π^{0}_{1}-conservativity,
local interpretability, Σ^{0}_{1}-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** +
{Con^{n}(**PA**); *n*∈*ω*}),
PRL(**ZFC**,**ZFC** + *CH*). (Here
Con^{n}(*T*) is the iterated consistency
assertion for *T*: Con^{1}(*T*) = Con(*T*),
Con^{n+1}(*T*) = Con(*T* + Con^{n}(*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:

- two sorts of formulas, corresponding (under the “arithmetical” realization) to the two first-order languages of the theories in question,
- two modal operators, each one applicable only to formulas of one sort, corresponding to the two provability predicates of our theories,
- an additional sort-switching operator, which corresponds to one of our interpretations of the first theory in the second one.

(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:

- Both of these theories are
simple enough, their metamathematical properties were
thoroughly studied, especially in the case of
**PA**. - In
**AST**there are two canonical natural interpretations of**PA**, given by the class of the*natural numbers*(**N**) and its proper initial segment, the class of the so-called*finite natural numbers*(**FN**). Note that this is a common situation in theories, formalizing some sort of the Nonstandard Analysis: there we have the (standard set of) internal natural numbers, which form a proper end-extension of the (external set of) standard natural numbers. However in such theories, this end-extension is usually elementary (by the Transfer Principle), which means that both types of numbers generate provably equivalent interpretations of arithmetic and are indistinguishable by means of the provability logic. We will see that this is not the case in**AST**, the interpretations given by**N**and**FN**behave very differently. - Of course, there were also personal reasons. I like
**AST**and I was aware of some strange-looking modal-like principles governing the interplay of**N**and**FN**, therefore I supposed it would be interesting to study it more deeply.

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.

- [Bek94]
- Lev D. Beklemishev,
*On bimodal logics of provability*, Annals of Pure and Applied Logic 68 (1994), no. 2, pp. 115–159. - [Bek96]
- Lev D. Beklemishev,
*Bimodal logics for extensions of arithmetical theories*, Journal of Symbolic Logic 61 (1996), no. 1, pp. 91–124. - [Car86]
- Tim Carlson,
*Modal logics with several operators and provability interpretations*, Israel Journal of Mathematics 54 (1986), no. 1, pp. 14–24.

Back to the main page