Gentzen-type formulation of the propositional logic LQ (Q1111545): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: A cut-free Gentzen-type system for the logic of the weak law of excluded middle / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Untersuchungen über das logische Schliessen. I / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Pseudo two-valued evaluation method for intermediate logics / rank | |||
Normal rank |
Latest revision as of 10:49, 19 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Gentzen-type formulation of the propositional logic LQ |
scientific article |
Statements
Gentzen-type formulation of the propositional logic LQ (English)
0 references
1988
0 references
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.
0 references
sequent calculi
0 references
intermediate logic
0 references
cut-elemination
0 references