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 | |||
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
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