Global properties of canonical derivability predicates in Peano Arithmetic) are studied here by means of a suitable propositional modal logic GL. A whole book [1] has appeared on GL and we refer to it for more information and a bibliography on GL. Here we propose a sequent calculus for GL and, by exhibiting a good proof procedure, prove that such calculus admits the elimination of cuts. Most of standard results on GL are then easy consequences: completeness, decidability, finite model property, (...) interpolation and the fixed point theorem. (shrink)

We introduce a Gentzen-style modal predicate logic and prove the cut-elimination theorem for it. This sequent calculus of cut-free proofs is chosen as a proxy to develop the proof-theory of the logics introduced in [14, 15, 4]. We present syntactic proofs for all the metatheoretical results that were proved model-theoretically in loc. cit. and moreover prove that the form of weak reflection proved in these papers is as strong as possible.

We introduce a new axiomatic system of modal logic, BM, extending classical first order logic by adding the binary modal symbol “▹” intended to simulate the metamathematical provability predicate “⊢” of classical logic. We demonstrate via examples how BM can be used to write equational proofs of first order classical theorems, and show that this ability hinges on a “conservation result”: BM proves A ▹ B for classical A and B iff A ⊢ B holds classically. We introduce appropriate Kripke (...) semantics with respect to which we prove BM is sound and complete. As a corollary we prove the above mentioned conservation result. (shrink)