Normalization and excluded middle. I (Q583185): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
Property / 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. | |||
Property / 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. / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B20 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F05 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B05 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03B10 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 4132123 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
classical logic | |||
Property / zbMATH Keywords: classical logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
intuitionistic logic | |||
Property / zbMATH Keywords: intuitionistic logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
law of the excluded middle | |||
Property / zbMATH Keywords: law of the excluded middle / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
normalization | |||
Property / zbMATH Keywords: normalization / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
minimal logic | |||
Property / zbMATH Keywords: minimal logic / rank | |||
Normal rank |
Revision as of 19:17, 1 July 2023
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