TR-2006003: Explicit Proofs in Formal Provability Logic
Evan Goris · CUNY Academic Works (City University of New York) · 2006
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 ∩ GL and equals the fragment that can be realized by proof-terms of LP.Additionally we show that the problem of determining which implicit provability assertions in a given modal formula can be made explicit is decidable.In the final sections of this paper we establish the disjunction property for GLA and give an axiomatization for GL ∩ S4.