Logic of proofs and provability (Q5957921)

Artemov's logic LP of proofs is extended by adjoining the GL modality so as to incorporate both the modality for provability and the operator representing the proof predicate ``is a proof of''. To formalize the joint logic, two new operations on proof terms are required for the language in addition to the ``application'', ``proof checker'', and ``choice'' of LP. The author gives an axiomatization of the logic, which is shown to be complete, with respect to the intended arithmetical provability interpretations as well as to the Kripke-type semantics, to be decidable, and to enjoy a kind of functional completeness on proof terms meaning that any invariant operation on proofs admitting description in the modal propositional language can be realized by a proof polynomial.