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)