An operational logic of proofs with positive and negative information (Q1970597)

As a generalization of provability logic, which deals with formal provability, Artemov introduced a dynamic logic in order to study the concept of proof in a formal way. Inspired by this idea, the authors investigate some natural operations on proofs based on the arithmetical interpretation and formalize some fragment of such kind of logic of proofs, which then is shown to be complete and decidable with respect to the arithmetical interpretation. An important advantage of the system in this paper compared to Artemov's original logic is that it is given by considering not only positive but also negative imformations on proofs such as ``not being a proof'', for instance.