Vol. 15 No. 4, © The Author, 2005. Published by Oxford University Press. All rights reserved.
Original Articles |
A Finitary Treatment of the Closed Fragment of Japaridze's Provability Logic
1 Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands. Email: lev{at}phil.uu.nl, jjoosten{at}phil.uu.nl, 2 FNWI, ILLC, Universiteit van Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands. Email: vervoort{at}science.uva.nl
We study a propositional polymodal provability logic GLP introduced by G. Japaridze. Previous treatments of this logic, due to Japaridze and Ignatiev, heavily relied on some non-finitary principles such as transfinite induction up to 
0 or reflection principles. In fact, the closed fragment of GLP gives rise to a natural system of ordinal notation for 0 that was used for a proof-theoretic analysis of Peano arithmetic and for constructing simple combinatorial independent statements. In this paper, we study Ignatiev's universal model for the closed fragment of this logic. Using bisimulation techniques, we show that several basic results on the closed fragment of GLP, including the normal form theorem, can be proved by purely finitary means formalizable in elementary arithmetic. As a corollary, the system of ordinal notation for 0 based on the closed fragment of GLP is shown to be provably isomorphic to the standard system of ordinal notation up to 0. We also settle negatively some conjectures by Ignatiev.
Received May 2005.