Marin, S;
Miller, D;
Pimentel, E;
Volpe, M;
(2022)
From axioms to synthetic inference rules via focusing.
Annals of Pure and Applied Logic
, 173
(5)
, Article 103091. 10.1016/j.apal.2022.103091.
Preview |
Text
1-s2.0-S0168007222000057-main.pdf - Accepted Version Download (1MB) | Preview |
Abstract
An important application of focused variants of Gentzen's sequent calculus proof rules is the construction of (possibly) large synthetic inference rules. This paper examines the synthetic inference rules that arise when using theories composed of bipolars, and we do this in both classical and intuitionistic logics. A key step in transforming a formula into synthetic inference rules involves attaching a polarity to atomic formulas and some logical connectives. Since there are different choices in how polarity is assigned, it is possible to produce different synthetic inference rules for the same formula. We show that this flexibility allows for the generalization of different approaches for transforming axioms into sequent rules present in the literature. We finish the paper showing how to apply these results to organize the proof theory of labeled sequent systems for several propositional modal logics.
| Type: | Article |
|---|---|
| Title: | From axioms to synthetic inference rules via focusing |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1016/j.apal.2022.103091 |
| Publisher version: | https://doi.org/10.1016/j.apal.2022.103091 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Synthetic inference rules, Polarities, Focusing, Axioms, Classical logic, Intuitionistic logic, Modal logics |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10142554 |
Archive Staff Only
 |
View Item |
