Gentzen-type formulation of the propositional logic LQ (Q1111545): Difference between revisions

LQ is the intermediate logic obtained by adding \(\neg A\vee \neg \neg A\) to intuitionistic logic LI. Presupposing familiarity with Gentzen's formulation of LI as LJ the author proposes a sequent version GQ of LQ by listing two sequents and a rule for readers to add to LJ. The sequents are (BL): \(A\to\), and (BR): \(\to A\). The rule is called WEM: \(\Gamma\to \Sigma\), \(\Gamma\to \Sigma /\Gamma \to \Sigma\). These additions are accompanied with syntactic restrictions, unmotivated by semantic considerations, for avoiding contradictions. By syntactic means it is shown that GQ\(=\)LQ and that GQ has cut-elemination.