Kürbis, Nils;
(2021)
Normalisation and Subformula Property for
a System of Intuitionistic Logic with General Introduction and Elimination Rules.
CoRR
, abs
, Article 2108.05842. 10.48550/arXiv.2110.09921.
Preview |
Text
KurbisGenIntroRulesInt.pdf - Accepted Version Download (172kB) | Preview |
Abstract
This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of `maximal formula', `segment' and `maximal segment' suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions in normal form have the subformula property.
| Type: | Article |
|---|---|
| Title: | Normalisation and Subformula Property for a System of Intuitionistic Logic with General Introduction and Elimination Rules |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.48550/arXiv.2110.09921 |
| Publisher version: | https://dblp.org/rec/journals/corr/abs-2108-05842 |
| Language: | English |
| Additional information: | The Creative Commons Public Domain Dedication waiver (http://creativecommons.org/publicdomain/zero/1.0/) applies to the data made available in this article, unless otherwise stated. |
| Keywords: | Intuitionistic logic, Proof theory, Normalisation, General elimination rules, General introduction rules, Harmony, Stability |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL SLASH UCL > Provost and Vice Provost Offices > UCL SLASH > Faculty of Arts and Humanities UCL > Provost and Vice Provost Offices > UCL SLASH > Faculty of Arts and Humanities > Dept of Philosophy |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10195681 |
Archive Staff Only
 |
View Item |
