zbMATH — the first resource for mathematics

Explicit proofs in formal provability logic. (English) Zbl 1133.03039
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 241-253 (2007).
Summary: In this paper we answer the question what implicit proof assertions in the provability logic GL can be realized by explicit proof terms. In particular we show that the fragment of GL which can be realized by generalized proof terms of GLA is exactly S4 \(\cap \) GL and equals the fragment that can be realized by proof-terms of LP. In the final sections of this paper we establish the disjunction property for GLA and give an axiomatization for GL \(\cap \) S4.
For the entire collection see [Zbl 1121.03005].
Reviewer: Reviewer (Berlin)

03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
Full Text: DOI