×

Calibrating provability logic: from modal logic to reflection calculus. (English) Zbl 1331.03040

Bolander, Thomas (ed.) et al., Advances in modal logic. Vol. 9. Proceedings of the 9th conference (AiML 2012), Copenhagen, Denmark, August 22–25, 2012. London: College Publications (ISBN 978-1-84890-068-4/pbk). 89-94 (2012).
In this paper, Beklemishev reports on progress in applying provability logics to ordinal analysis. The polymodal provability logic \(\mathsf {GLP}\) has been applied to perform an ordinal analysis for theories like Peano Arithmetic (\(\mathsf {PA}\)). Although \(\mathsf {GLP}\) is decidable it is not as well-behaved as other modal logics. In particular, it is known to not be complete with respect to any class of frames.
Recent developments have shown that the ordinal analysis can actually be performed in a rather weak fragment of \(\mathsf {GLP}\). This fragment is called Reflection Calculus (\(\mathsf {RC}\)) and its closed fragment \(\mathsf {RC}^0\) and the paper gives an overview of its main applications. Instead of presenting any proofs, the paper provides the necessary pointers to the literature. The calculus is called \(\mathsf {RC}\) since the modal operators are interpreted as natural reflection principles (if provable then true).
It is mentioned how \(\mathsf {RC}^0\) can be used to represent ordinals below \(\varepsilon_0\). Also it can be used to denote standard fragments of arithmetic. Conservativity results for rather natural fragments of arithmetic can thus be stated using \(\mathsf {RC}^0\) by calling upon the so-called reduction property.
Putting all pieces together – \(\mathsf {RC}^0\) as a modal logic; \(\mathsf {RC}^0\) representing subtheories of \(\mathsf {PA}\); \(\mathsf {RC}^0\) representing ordinals – it is shown how the calculus can be set to work to give a consistency proof of \(\mathsf {PA}\) à la Gentzen. It is mentioned that this gives rise to a true combinatorial principle – called Every Worm Dies – that is independent of \(\mathsf {PA}\).
For the entire collection see [Zbl 1262.03005].

MSC:

03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03B45 Modal logic (including the logic of norms)
PDFBibTeX XMLCite