Proof internalization in generalized Frege systems for classical logic (Q392294): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
Normalize DOI.
 
(4 intermediate revisions by 4 users not shown)
Property / DOI
 
Property / DOI: 10.1016/j.apal.2013.07.017 / rank
Normal rank
 
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1016/j.apal.2013.07.017 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W1964468701 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Logic of proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Explicit Provability and Constructive Semantics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Deep sequent systems for modal logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2904046 / rank
 
Normal rank
Property / DOI
 
Property / DOI: 10.1016/J.APAL.2013.07.017 / rank
 
Normal rank

Latest revision as of 16:15, 9 December 2024

scientific article
Language Label Description Also known as
English
Proof internalization in generalized Frege systems for classical logic
scientific article

    Statements

    Proof internalization in generalized Frege systems for classical logic (English)
    0 references
    0 references
    13 January 2014
    0 references
    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.
    0 references
    provability logic
    0 references
    justification logic
    0 references
    modal logic
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references