Proof internalization in generalized Frege systems for classical logic (Q392294)

The paper offers a generalised approach to problems which are dealt with by the logic of proofs (or justification logic) invented by Artemov and being a generalization of modal provability logic. In particular, justification logic allows for dealing with propositions and proofs in the same language by means of so called proof polynomials which serve as templates for proofs. One can avoid in this way the problem of logical omniscience. The main problem in justification logics is with so called realization theorems which specify how to replace boxes in modal formulas with corresponding justifications. In the paper, the notion of generalised Frege system is introduced which allows for direct syntactical manipulation on proofs themselves, not their templates (proof polynomials). In this way we obtain systems that can internalize their own proofs. In Section 2, generalised Frege systems are described satisfying very general criteria (deduction and resolution property) and it is shown how to represent (translate) a logic in such a system. Internalization of proofs and nested structures are discussed first in an abstract way. Next, two concrete proof systems: Hilbert-style axiom system and some sequent calculus for classical logic are examined as examples of the application of the presented approach. Finally, the realization theorems for both example systems are proved and some generalizations are briefly discussed. The paper is of interest for students in proof theory and provability logic.