Gentzen-type formulation of the propositional logic LQ
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.
- scientific article; zbMATH DE number 1157127
- The Gentzen-Kripke construction of the intermediate logic LQ
- Gentzen calculi for modal propositional logic
- Propositional Q-logic
- scientific article; zbMATH DE number 4031641
- scientific article; zbMATH DE number 3871327
- scientific article; zbMATH DE number 5257967
- Gentzen-style axiomatizations in equational logic
- scientific article; zbMATH DE number 1696769
- scientific article; zbMATH DE number 1453079
- A cut-free Gentzen-type system for the logic of the weak law of excluded middle
- The Gentzen-Kripke construction of the intermediate logic LQ
- Intermediate logics admitting a structural hypersequent calculus
- MULTIPLE FORMS OF GENTZEN'S RULES AND SOME INTERMEDIATE LOGICS
- On the Logical System L1
- scientific article; zbMATH DE number 1157127 (Why is no real title available?)
- scientific article; zbMATH DE number 786494 (Why is no real title available?)
This page was built for publication: Gentzen-type formulation of the propositional logic LQ
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1111545)
