Kurbis, N;
(2021)
Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules.
Synthese
10.1007/s11229-021-03418-8.
(In press).
Preview |
Text
Kurbis_Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules_AOP.pdf - Published Version Download (375kB) | 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.1007/s11229-021-03418-8 |
Publisher version: | https://doi.org/10.1007/s11229-021-03418-8 |
Language: | English |
Additional information: | © 2021 Springer Nature Switzerland AG. This article is licensed under a Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/). |
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/10137258 |




Archive Staff Only
![]() |
View Item |