Operations on Proofs That Can be Specified by Means of Modal Logic
Sergei Nikolaevich Artemov · 1999
Explicit modal logic was first sketched by Gödel in [16] as the logic with the atoms "t is a proof of F". The complete axiomatization of the Logic of Proofs LP was found in [4] (see also [6],[7],[18]). In this paper we establish a sort of a functional completeness property of proof polynomials which constitute the system of proof terms in LP. Proof polynomials are built from variables and constants by three operations on proofs: "\\Delta" (application), "!" (proof checker), and "+" (choice). Here constants stand for canonical proofs of "simple facts", namely instances of propositional axioms and axioms of LP in a given proof system. We show that every operation on proofs that (i) can be specified in a propositional modal language and (ii) is invariant with respect to the choice of a proof system is realized by a proof polynomial.