• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Глава

Calibrating Provability Logic: From Modal Logic to Re ection Calculus

P. 89-94.

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.

В книге

Под науч. редакцией: T. Bolander, T. Brauner, S. Ghilardi. Iss. 9. L.: College Publications, 2012.