Normalization and excluded middle. I (Q583185): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
(4 intermediate revisions by 4 users not shown) | |||
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 | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5802120 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The system LD / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5547552 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5579475 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5559220 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5632554 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the proof theory of the intermediate logic MH / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Intensional interpretations of functionals of finite type I / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/bf02770512 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2036407372 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 09:28, 30 July 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