Reference Constructions in the Single-conclusion Proof Logic
Vladimir Nikolaevich Krupski · Journal of Logic and Computation · 2006
We propose an extension of the propositional proof logic language by the second-order variables denoting the reference constructors (like ‘the formula which is proven by x’). The proof logic in this weak second-order language is axiomatized via the calculus ref, the (Functional) Logic of Proofs with References. It is supplied with the formal arithmetical semantics: we prove that ref is sound with respect to arithmetical interpretations and is a conservative extension of propositional single-conclusion proof logic . Finally, we demonstrate how the language of ref can be used as a scheme language for arithmetic and provide the corresponding proof conversion method.