Normalization and excluded middle. I
type: Item
instance of: scholarly article
title: Normalization and excluded middle. I
zbMATH Open document ID: 0692.03007
DOI: 10.1007/BF02770512
author: Jonathan P. Seldin
published in: Studia Logica
publication date: 1989-01-01T00:00:00Z
review text: The rule \[ \supset K:\quad \Gamma,\quad \neg A\vdash A\quad \to \quad \Gamma \vdash A \] is precisely strong enough to give classical logic from intuitionistic logic, and thus it is exactly equivalent to the law of the excluded middle. This rule is a special case of the rule: \[ \neg D:\quad \Gamma,\quad A\supset B\vdash A\quad \to \quad \Gamma \vdash A. \] The main result of the paper is to prove the normalization theorem for deductions in the propositional logics and first order predicate logics obtained from intuitionistic logic or minimal logic by adding one of these rules. Every deduction in these logics is shown to be reducible by complete \(\supset K\)-reductions to a \(\supset K\)-reduced deduction with the same undischarged assumptions and the same conclusion; and then, any \(\supset K\)-reduced deduction can be normalized by the methods used for intuitionistically based logic since each \(\supset K\)-reduced deduction has at most one inference by the rule \(\supset K\) and that, if it occurs, is at the end of the deduction.
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B05
Mathematics Subject Classification ID: 03B10
zbMATH DE Number: 4132123
zbMATH Keywords: classical logic
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: law of the excluded middle
zbMATH Keywords: normalization
zbMATH Keywords: minimal logic
MaRDI profile type: Publication
cites work: Q5802120
cites work: The system LD
cites work: Q5547552
cites work: Q5579475
cites work: Q5559220
cites work: Q5632554
cites work: On the proof theory of the intermediate logic MH
cites work: Intensional interpretations of functionals of finite type I
full work available at URL: https://doi.org/10.1007/bf02770512
OpenAlex ID: W2036407372
description: scientific article; zbMATH DE number 4132123