English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The Gentzen-Kripke construction of the semantics for intermedi- ate logic LQ, which is obtainable from the intuitionistic propositional logic H by adding the weak law of excluded middle -*A v —• —1>4, is presented. Our construction spans the Gentzen system and the Kripke semantics for LQ by providing the way from the cut-elimination theorem to model-theoretic re- sults. The completeness and decidability theorems are shown in this method. / Introduction An intermediate logic LQ is obtainable from the intuitionis- tic propositional logic H by adding the weak law of excluded middle -\A v -»-vl. The logic can also be axiomatized by the axiom schema (-\A -> -ii?) v ( -ιB -> -ιA). The motivation of LQ is purely technical rather than philosophical in that LQ is one possible extension of H. Our interest thus lies in its characterization in relation to the formalization of H. The semantics for LQ can be given by the class of directed Kripke frames; see Gabbay (4). Several authors also proposed the Gentzen systems for LQ, none of which is successful. For example, the cut-elimination theorem cannot be proved in the sequent calculus of Boricic (2) as Hosoi pointed out. Recently, Hosoi (6) gave a Gentzen-type formulation GQ for LQ and proved the cut-elim- ination theorem. The purpose of this paper is to develop the Gentzen-Kripke construction of the semantics for LQ using the subformula models, as a modification of the one developed in Akama (1) for intuitionistic predicate logic. The proposed construc- tion spans the Gentzen system and the Kripke semantics for LQ by providing the way from the cut-elimination theorem to model-theoret ic results. The complete- ness and decidability theorems are shown in this method.

The Gentzen-Kripke construction of the intermediate logic LQ.