Normalization and excluded middle. I (Q583185): Difference between revisions
From MaRDI portal
Changed an Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 08:27, 30 January 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Normalization and excluded middle. I |
scientific article |
Statements
Normalization and excluded middle. I (English)
0 references
1989
0 references
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.
0 references
classical logic
0 references
intuitionistic logic
0 references
law of the excluded middle
0 references
normalization
0 references
minimal logic
0 references