A cut-free Gentzen-type system for the logic of the weak law of excluded middle (Q1100191): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Removed claim: reviewed by (P1447): Item:Q588143 |
||
| Property / reviewed by | |||
| Property / reviewed by: Osamu Sonobe / rank | |||
Revision as of 23:56, 19 February 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A cut-free Gentzen-type system for the logic of the weak law of excluded middle |
scientific article |
Statements
A cut-free Gentzen-type system for the logic of the weak law of excluded middle (English)
0 references
1986
0 references
The first order intermediate logic of the weak law of excluded middle \(\neg A\vee \neg \neg A\) is formulated in a Gentzen-type system, for which the cut elimination theorem is proved by the usual constructive method. As consequences the author gives the interpolation theorem, the decidability of the propositional part and so on.
0 references
proof theory
0 references
sequent calculus
0 references
intermediate logic
0 references
weak law of excluded middle
0 references
Gentzen-type system
0 references
cut elimination
0 references
interpolation theorem
0 references
