Аннотация:Explicit modal logic was first sketched by Gödel in 1938 as the logic with the atoms “t is a proof of F”. The complete axiomatization of the Logic of Proofs LP was found by Artemov in 1995. 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: “·” (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.
