Abstract

Logic of proofs LP was introduced by S. Artemov in. It describes properties of the proof predicate “t is a proof of F” formalized by the formula ⟦t⟧ F. Proofs are represented by terms constructed by three elementary recursive operations on proofs. In this paper we extend the language of the logic of proofs by the additional storage predicate x ∋ F with the intended interpretation “x is a label for F”. The storage predicate can play the role of syntax encoding, so it is useful for specification of operations on proofs, especially those that require formula arguments. We give a definition of a specification of an operation on proofs and introduce logics that describe such operations. For a large class of operations we prove the completeness of these logics with respect to the intended semantics. We also study the logic describing the operation of substitution.