No label defined (Q4329233)

The logic LP of proofs is a propositional logic provided for formalizing the notion of proof by making use of terms to express proofs formally and a predicate operating on a term \(t\) and a formula \(F\) which is intended to mean ``\(t\) is a proof of \(F\)''. In his previous works, the author established its complete axiomatization with respect to the standard arithmetical interpretation and gave a positive solution to the problem of finding the exact provability interpretation of the modal logic S4 suggested by Gödel, which at the same time supports Gödel's interpretation of intuitionistic logic by means of classical provability according to its embedding into S4. In this paper the author shows a kind of functional completeness of LP with respect to proof terms that are defined in the language for LP by three fundamental operators called ``application'', ``proof checker'', and ``choice'', respectively. The result means 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 constructed by the three fundamental operations. For the entire collection see [Zbl 0979.00027].