ИСТИНА

Several interesting applications of provability logic in proof theory made use of the polymodal logic GLP due to Giorgi Japaridze. This system, although decidable, is not very easy to handle. In this talk we will advocate the use of a weaker system, called Reflection Calculus, which is much simpler than GLP, yet expressive enough to regain its main proof-theoretic applications. 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 conjunction and the diamond modalities. We discuss general problems around weak systems of this kind, e.g. their relationships with semi-Thue systems, and describe some applications of RC to the analysis of provability in formal arithmetical theories.