Operations on Proofs That Can be Specified by Means of Modal Logic
CORNELL UNIV ITHACA NY CENTER FOR FOUNDATIONS OF INTELLIGENT SYSTEMS
Pagination or Media Count:
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.
- Theoretical Mathematics