Referential logic of proofs

AbstractWe introduce an extension of the propositional logic of single-conclusion proofs by the second-order variables denoting the reference constructors of the type “the formula which is proved by x.’’ The resulting Logic of Proofs with References, FLPref, is shown to be decidable, and to enjoy soundness and completeness with respect to the intended provability semantics. We show that FLPref provides a complete test of admissibility of inference rules in a sound extension of arithmetic. This paper may be regarded as a contribution to the theory of automated reasoning systems