?
Calibrating Provability Logic: From Modal Logic to Re ection Calculus
Several interesting applications of provability logic in proof theory made use of a polymodal logic GLP due to Giorgi Japaridze. This system, although de- cidable, is not very easy to handle. In particular, it is not Kripke complete. It is complete w.r.t. neighborhood semantics, however this could only be established recently by rather complicated techniques [1]. In this talk we will advocate the use of a weaker system, called Re ection Calculus, which is much simpler than GLP, yet expressive enough to regain its main proof-theoretic applications, and more. From the point of view of modal logic, RC can be seen as a fragment of polymodal logic consisting of implications of the form A ! B, where A and B are formulas built-up from > and the variables using just ^ and the diamond modalities. In this paper we formulate it in a somewhat more succinct self-contained format. Further, we state its arithmetical interpretation, and provide some evidence that RC is much simpler than GLP. We then outline a consistency proof for Peano arithmetic based on RC and state a simple combinatorial statement, the so-called Worm principle, that was suggested by the use of GLP but is even more directly related to the Re ection Calculus.