Negative operations on proofs and labels

Abstract

Logic of proofs LP introduced by S. Artemov in 1995 describes properties of proof predicate “t is a proof of F” in the propositional language extended by atoms of the form [[t]F. Proof are represented by terms constructed by three elementary recursive operations on proofs. In order to make the language more expressive we introduce the additional storage predicate with the intended interpretation “x is a label for F”. It can play the role of syntax encoding, so it is useful for specification of operations that require formula arguments. In this paper we study operations on proofs and labels that can be specified in the extended language. First, we give a formal definition of an operation on proofs and labels. Then, for an arbitrary finite set of operations F the logic LPS(F) is defined. We provide LPS(F) with symbolic semantics and arithmetical semantics. The main result of the paper is the uniform completeness theorem for this family of logics with respect to the both types of semantics.