A cut-free Gentzen-type system for the logic of the weak law of excluded middle
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.
scientific article; zbMATH DE number 4041875