Explicit modal logic was first sketched by Goedel 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, and 21). 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: (1) can be specified in a propositional modal language, and (2) is invariant with respect to the choice of a proof system is realized by a proof polynomial.
