Arrow Research search

Author name cluster

Norihiro Kamide

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

11 papers
2 author rows

Possible papers

11

FLAP Journal 2025 Journal Article

Alternative Cut-free Sequent Calculi for S4 that are Compatible with Paradefinite Four-valued Logic

  • Norihiro Kamide

Three new Gentzen-style sequent calculi GS41, GS42, and GS43 for normal modal logic S4 are introduced. These calculi are obtained from a Gentzen-style sequent calculus GMA4 for a modal extension MA4 of Avron’s self-extensional paradefinite four-valued logic by adding some special inference rules and/or some special initial sequents. The cut-elimination theorems for GS41, GS42, GS43, and GMA4 are proved. An alternative Kripke semantics for S4 is intro- duced and the completeness theorems with respect to this semantics are proved for GS41 and GS42. An extended Kripke semantics is introduced for an ex- tended S4 with an auxiliary negation connective and the completeness theorem with respect to this semantics is proved for GS43. Finally, a Gödel–McKinsey– Tarski theorem for embedding Gurevich logic into S4 is proved.

PDF Details

FLAP Journal 2023 Journal Article

Embedding First-order Classical Logic into Gurevich's Extended First-order Intuitionistic Logic: The Role of Strong Negation.

  • Norihiro Kamide

In this study, a theorem for embedding first-order classical logic into Gure- vich’s extended first-order intuitionistic logic with strong negation is investi- gated in terms of the Gödel–Gentzen negative translation. First, an alternative cut-free Gentzen-style sequent calculus ELK for first-order classical logic is in- troduced to extend Gentzen’s sequent calculus LK for first-order classical logic. Second, a theorem for embedding ELK into a Gentzen-style sequent calculus ELJ for Gurevich’s extended first-order intuitionistic logic with strong negation is proved using an extended Gödel–Gentzen negative translation. Finally, a theorem for embedding ELK into Gentzen’s sequent calculus LJ for first-order intuitionistic logic is obtained using a slightly modified version of the extended Gödel–Gentzen negative translation.

PDF Details

FLAP Journal 2020 Journal Article

Cut-elimination, Completeness and Craig Interpolation Theorems for Gurevich's Extended First-order Intuitionistic Logic with Strong Negation.

  • Norihiro Kamide

Gurevich’s extended first-order intuitionistic logic with strong negation (GI) is defined as a new Gentzen-type sequent calculus. The logic GI is also known to be an extension of Nelson’s first-order constructive three-valued logic N3 by adding intuitionistic negation. The cut-elimination, completeness, and Craig interpolation theorems for GI are proved using some theorems for embedding GI into first-order intuitionistic logic.

Details

LORI Conference 2017 Conference Paper

An Extended First-Order Belnap-Dunn Logic with Classical Negation

  • Norihiro Kamide
  • Hitoshi Omori

Abstract In this paper, we investigate an extended first-order Belnap-Dunn logic with classical negation. We introduce a Gentzen-type sequent calculus FBD+ for this logic and prove theorems for syntactically and semantically embedding FBD+ into a Gentzen-type sequent calculus for first-order classical logic. Moreover, we show the cut-elimination theorem for FBD+ and prove the completeness theorems with respect to both valuation and many-valued semantics for FBD+.

Details

FLAP Journal 2016 Journal Article

Completeness of Connexive Heyting-Brouwer Logic.

  • Norihiro Kamide
  • Heinrich Wansing

In this paper, we investigate a logic called connexive Heyting-Brouwer logic or bi-intuitionistic connexive logic, BCL. The system BCL is introduced as a Gentzen-type sequent calculus, and we prove some theorems for embedding BCL into a Gentzen-type sequent calculus BL for bi-intuitionistic logic, BiInt. The completeness theorem with respect to a Kripke semantics for BCL is proved using these embedding theorems. The cut-elimination theorem and a certain duality principle are also shown for some subsystems of BCL. Moreover, we present a sound and complete triply-signed tableau calculus for BCL.

PDF Details

LORI Conference 2015 Conference Paper

A Decidable Temporal Relevant Logic for Time-Dependent Relevant Human Reasoning

  • Norihiro Kamide

Abstract In this paper, a Gentzen-type sequent calculus STRW is introduced for a new temporal relevant logic TRW which is obtained from the positive contraction-less relevant logic by adding some temporal operators. The cut-elimination and completeness theorems for STRW are proved. STRW is shown to be decidable and to have relevance principle.

Details

JELIA Conference 2008 Conference Paper

Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials

  • Norihiro Kamide

Abstract It is known that Girard’s linear logics can elegantly represent the concept of “resource consumption”. The linear exponential operator! in linear logics can express a specific infinitely reusable resource (i. e. , it is reusable not only for any number, but also many times). It is also known that the propositional intuitionistic linear logic with! and the first-order intuitionistic linear logic without! (called here ILL) are undecidable and decidable, respectively. In this paper, a new decidable first-order intuitionistic linear logic, called the resource-indexed linear logic RL[ l ], is introduced by extending and generalizing ILL. The logic RL[ l ] has an l -bounded exponential operator! l, and this operator can express a specific finitely usable resource (i. e. , it is usable in any positive number less than l + 1, but only once). The embedding theorem of RL[ l ] into ILL is proved, and by using this theorem, the cut-elimination and decidability theorems for RL[ l ] are shown.

Details