61 found
Order:
  1.  21
    Proof Theory of Paraconsistent Quantum Logic.Norihiro Kamide - 2018 - Journal of Philosophical Logic 47 (2):301-324.
    Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, is introduced as Gentzen-type sequent calculi, and the cut-elimination theorems for these calculi are proved. This logic is shown to be decidable through the use of these calculi. A first-order extension of this logic is also shown to be decidable. The relationship between minimal quantum logic and paraconsistent four-valued logic is clarified, and a survey of existing Gentzen-type sequent calculi for these logics and their close relatives is (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  2.  14
    Modal Multilattice Logic.Norihiro Kamide & Yaroslav Shramko - 2017 - Logica Universalis 11 (3):317-343.
    A modal extension of multilattice logic, called modal multilattice logic, is introduced as a Gentzen-type sequent calculus \. Theorems for embedding \ into a Gentzen-type sequent calculus S4C and vice versa are proved. The cut-elimination theorem for \ is shown. A Kripke semantics for \ is introduced, and the completeness theorem with respect to this semantics is proved. Moreover, the duality principle is proved as a characteristic property of \.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  3.  8
    Lattice Logic, Bilattice Logic and Paraconsistent Quantum Logic: a Unified Framework Based on Monosequent Systems.Norihiro Kamide - forthcoming - Journal of Philosophical Logic:1-31.
    Lattice logic, bilattice logic, and paraconsistent quantum logic are investigated based on monosequent systems. Paraconsistent quantum logic is an extension of lattice logic, and bilattice logic is an extension of paraconsistent quantum logic. Monosequent system is a sequent calculus based on the restricted sequent that contains exactly one formula in both the antecedent and succedent. It is known that a completeness theorem with respect to a lattice-valued semantics holds for a monosequent system for lattice logic. A completeness theorem with respect (...)
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  4.  23
    Kripke Completeness of Bi-Intuitionistic Multilattice Logic and its Connexive Variant.Norihiro Kamide, Yaroslav Shramko & Heinrich Wansing - 2017 - Studia Logica 105 (6):1193-1219.
    In this paper, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can be regarded as a bi-intuitionistic variant of the original classical multilattice logic (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  12
    Gentzen-Type Sequent Calculi for Extended Belnap–Dunn Logics with Classical Negation: A General Framework.Norihiro Kamide - 2019 - Logica Universalis 13 (1):37-63.
    Gentzen-type sequent calculi GBD+, GBDe, GBD1, and GBD2 are respectively introduced for De and Omori’s axiomatic extensions BD+, BDe, BD1, and BD2 of Belnap–Dunn logic by adding classical negation. These calculi are constructed based on a small modification of the original characteristic axiom scheme for negated implication. Theorems for syntactically and semantically embedding these calculi into a Gentzen-type sequent calculus LK for classical logic are proved. The cut-elimination, decidability, and completeness theorems for these calculi are obtained using these embedding theorems. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6.  62
    Sequent Calculi for Some Trilattice Logics.Norihiro Kamide & Heinrich Wansing - 2009 - Review of Symbolic Logic 2 (2):374-395.
    The trilattice SIXTEEN3 introduced in Shramko & Wansing (2005) is a natural generalization of the famous bilattice FOUR2. Some Hilbert-style proof systems for trilattice logics related to SIXTEEN3 have recently been studied (Odintsov, 2009; Shramko & Wansing, 2005). In this paper, three sequent calculi GB, FB, and QB are presented for Odintsovs coordinate valuations associated with valuations in SIXTEEN3. The equivalence between GB, FB, and QB, the cut-elimination theorems for these calculi, and the decidability of B are proved. In addition, (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  7.  14
    Paraconsistent Double Negations as Classical and Intuitionistic Negations.Norihiro Kamide - 2017 - Studia Logica 105 (6):1167-1191.
    A classical paraconsistent logic, which is regarded as a modified extension of first-degree entailment logic, is introduced as a Gentzen-type sequent calculus. This logic can simulate the classical negation in classical logic by paraconsistent double negation in CP. Theorems for syntactically and semantically embedding CP into a Gentzen-type sequent calculus LK for classical logic and vice versa are proved. The cut-elimination and completeness theorems for CP are also shown using these embedding theorems. Similar results are also obtained for an intuitionistic (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  8.  9
    Extending Paraconsistent Quantum Logic: A Single-Antecedent/Succedent System Approach.Norihiro Kamide - 2018 - Mathematical Logic Quarterly 64 (4-5):371-386.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  9.  12
    Combining Linear-Time Temporal Logic with Constructiveness and Paraconsistency.Norihiro Kamide & Heinrich Wansing - 2010 - Journal of Applied Logic 8 (1):33-61.
  10.  23
    Quantized Linear Logic, Involutive Quantales and Strong Negation.Norihiro Kamide - 2004 - Studia Logica 77 (3):355-384.
    A new logic, quantized intuitionistic linear logic, is introduced, and is closely related to the logic which corresponds to Mulvey and Pelletier's involutive quantales. Some cut-free sequent calculi with a new property quantization principle and some complete semantics such as an involutive quantale model and a quantale model are obtained for QILL. The relationship between QILL and Wansing's extended intuitionistic linear logic with strong negation is also observed using such syntactical and semantical frameworks.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  11.  24
    A Note on Dual-Intuitionistic Logic.Norihiro Kamide - 2003 - Mathematical Logic Quarterly 49 (5):519.
    Dual-intuitionistic logics are logics proposed by Czermak , Goodman and Urbas . It is shown in this paper that there is a correspondence between Goodman's dual-intuitionistic logic and Nelson's constructive logic N−.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  12.  85
    Kripke Semantics for Modal Substructural Logics.Norihiro Kamide - 2002 - Journal of Logic, Language and Information 11 (4):453-470.
    We introduce Kripke semantics for modal substructural logics, and provethe completeness theorems with respect to the semantics. Thecompleteness theorems are proved using an extended Ishihara's method ofcanonical model construction (Ishihara, 2000). The framework presentedcan deal with a broad range of modal substructural logics, including afragment of modal intuitionistic linear logic, and modal versions ofCorsi's logics, Visser's logic, Méndez's logics and relevant logics.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  13.  37
    A Relationship Between Rauszer's HB Logic and Nelson's Logic'.Norihiro Kamide - 2004 - Bulletin of the Section of Logic 33 (4):237-249.
  14.  42
    Gentzen-Type Methods for Bilattice Negation.Norihiro Kamide - 2005 - Studia Logica 80 (2-3):265-289.
    A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  15.  28
    A Hierarchy of Weak Double Negations.Norihiro Kamide - 2013 - Studia Logica 101 (6):1277-1297.
    In this paper, a way of constructing many-valued paraconsistent logics with weak double negation axioms is proposed. A hierarchy of weak double negation axioms is addressed in this way. The many-valued paraconsistent logics constructed are defined as Gentzen-type sequent calculi. The completeness and cut-elimination theorems for these logics are proved in a uniform way. The logics constructed are also shown to be decidable.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  16.  10
    Sequent Calculi for Intuitionistic Linear Logic with Strong Negation.Norihiro Kamide - 2002 - Logic Journal of the IGPL 10 (6):653-678.
    We introduce an extended intuitionistic linear logic with strong negation and modality. The logic presented is a modal extension of Wansing's extended linear logic with strong negation. First, we propose three types of cut-free sequent calculi for this new logic. The first one is named a subformula calculus, which yields the subformula property. The second one is termed a dual calculus, which has positive and negative sequents. The third one is called a triple-context calculus, which is regarded as a natural (...)
    Direct download  
     
    Export citation  
     
    Bookmark   8 citations  
  17.  36
    Proof Systems Combining Classical and Paraconsistent Negations.Norihiro Kamide - 2009 - Studia Logica 91 (2):217-238.
    New propositional and first-order paraconsistent logics (called L ω and FL ω , respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding theorems of L ω and FL ω into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple semantics for L ω and FL ω are proved. The cut-elimination theorems for L ω and FL ω are shown using both syntactical ways via the embedding theorems and semantical ways (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  18.  33
    Phase Semantics and Petri Net Interpretation for Resource-Sensitive Strong Negation.Norihiro Kamide - 2006 - Journal of Logic, Language and Information 15 (4):371-401.
    Wansing’s extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson’s constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke semantics, (3) a cut-free sequent calculus for WILL, called twist (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  19.  14
    A Cut-Free System for 16-Valued Reasoning.Norihiro Kamide - 2005 - Bulletin of the Section of Logic 34 (4):213-226.
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  20.  16
    Paraconsistent Double Negation as a Modal Operator.Norihiro Kamide - 2016 - Mathematical Logic Quarterly 62 (6):552-562.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  21.  36
    Normal Modal Substructural Logics with Strong Negation.Norihiro Kamide - 2003 - Journal of Philosophical Logic 32 (6):589-612.
    We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  22.  11
    Synthesized Substructural Logics.Norihiro Kamide - 2007 - Mathematical Logic Quarterly 53 (3):219-225.
    A mechanism for combining any two substructural logics (e.g. linear and intuitionistic logics) is studied from a proof-theoretic point of view. The main results presented are cut-elimination and simulation results for these combined logics called synthesized substructural logics.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  23.  41
    Substructural Logics with Mingle.Norihiro Kamide - 2002 - Journal of Logic, Language and Information 11 (2):227-249.
    We introduce structural rules mingle, and investigatetheorem-equivalence, cut- eliminability, decidability, interpolabilityand variable sharing property for sequent calculi having the mingle.These results include new cut-elimination results for the extendedlogics: FLm (full Lambek logic with the mingle), GLm(Girard's linear logic with the mingle) and Lm (Lambek calculuswith restricted mingle).
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  24.  45
    Substructural Implicational Logics Including the Relevant Logic E.Ryo Kashima & Norihiro Kamide - 1999 - Studia Logica 63 (2):181-212.
    We introduce several restricted versions of the structural rules in the implicational fragment of Gentzen's sequent calculus LJ. For example, we permit the applications of a structural rule only if its principal formula is an implication. We investigate cut-eliminability and theorem-equivalence among various combinations of them. The results include new cut-elimination theorems for the implicational fragments of the following logics: relevant logic E, strict implication S4, and their neighbors (e.g., E-W and S4-W); BCI-logic, BCK-logic, relevant logic R, and the intuitionistic (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  25.  33
    An Embedding-Based Completeness Proof for Nelson's Paraconsistent Logic.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (3/4):205-214.
  26.  27
    Symmetric and Dual Paraconsistent Logics.Norihiro Kamide & Heinrich Wansing - 2010 - Logic and Logical Philosophy 19 (1-2):7-30.
    Two new first-order paraconsistent logics with De Morgan-type negations and co-implication, called symmetric paraconsistent logic (SPL) and dual paraconsistent logic (DPL), are introduced as Gentzen-type sequent calculi. The logic SPL is symmetric in the sense that the rule of contraposition is admissible in cut-free SPL. By using this symmetry property, a simpler cut-free sequent calculus for SPL is obtained. The logic DPL is not symmetric, but it has the duality principle. Simple semantics for SPL and DPL are introduced, and the (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  27.  17
    Notes on Craig Interpolation for LJ with Strong Negation.Norihiro Kamide - 2011 - Mathematical Logic Quarterly 57 (4):395-399.
    The Craig interpolation theorem is shown for an extended LJ with strong negation. A new simple proof of this theorem is obtained. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  28.  45
    Dynamic Non-Commutative Logic.Norihiro Kamide - 2010 - Journal of Logic, Language and Information 19 (1):33-51.
    A first-order dynamic non-commutative logic, which has no structural rules and has some program operators, is introduced as a Gentzen-type sequent calculus. Decidability, cut-elimination and completeness theorems are shown for DN or its fragments. DN is intended to represent not only program-based, resource-sensitive, ordered, sequence-based, but also hierarchical reasoning.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  29.  11
    Phase Semantics for Linear-Time Formalism.Norihiro Kamide - 2011 - Logic Journal of the IGPL 19 (1):121-143.
    It is known that linear-time temporal logic is a useful logic for verifying and specifying concurrent systems. In this paper, phase semantics for LTL and its substructural refinements is introduced, and the completeness and cut-elimination theorems for LTL and its refinements are proved based on this semantics.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  30.  13
    Completeness and Cut-Elimination Theorems for Trilattice Logics.Norihiro Kamide & Heinrich Wansing - 2011 - Annals of Pure and Applied Logic 162 (10):816-835.
    A sequent calculus for Odintsov’s Hilbert-style axiomatization of a logic related to the trilattice SIXTEEN3 of generalized truth values is introduced. The completeness theorem w.r.t. a simple semantics for is proved using Maehara’s decomposition method that simultaneously derives the cut-elimination theorem for . A first-order extension of and its semantics are also introduced. The completeness and cut-elimination theorems for are proved using Schütte’s method.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  31.  25
    Natural Deduction Systems for Nelson's Paraconsistent Logic and its Neighbors.Norihiro Kamide - 2005 - Journal of Applied Non-Classical Logics 15 (4):405-435.
    Firstly, a natural deduction system in standard style is introduced for Nelson's para-consistent logic N4, and a normalization theorem is shown for this system. Secondly, a natural deduction system in sequent calculus style is introduced for N4, and a normalization theorem is shown for this system. Thirdly, a comparison between various natural deduction systems for N4 is given. Fourthly, a strong normalization theorem is shown for a natural deduction system for a sublogic of N4. Fifthly, a strong normalization theorem is (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  32.  12
    A Spatial Modal Logic with a Location Interpretation.Norihiro Kamide - 2005 - Mathematical Logic Quarterly 51 (4):331.
    A spatial modal logic is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut-elimination theorem for a modified subsystem of SML are also presented.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  33.  19
    A Note on Decision Problems for Implicational Sequent Calculi.Norihiro Kamide - 2001 - Bulletin of the Section of Logic 30 (3):129-138.
  34. Automating and Computing Paraconsistent Reasoning: Contraction-Free, Resolution and Type Systems.Norihiro Kamide - 2010 - Reports on Mathematical Logic:3-21.
     
    Export citation  
     
    Bookmark  
  35.  4
    A Decidable Paraconsistent Relevant Logic: Gentzen System and Routley-Meyer Semantics.Norihiro Kamide - 2016 - Mathematical Logic Quarterly 62 (3):177-189.
    In this paper, the positive fragment of the logic math formula of contraction-less relevant implication is extended with the addition of a paraconsistent negation connective similar to the strong negation connective in Nelson's paraconsistent four-valued logic math formula. This extended relevant logic is called math formula, and it has the property of constructible falsity which is known to be a characteristic property of math formula. A Gentzen-type sequent calculus math formula for math formula is introduced, and the cut-elimination and decidability (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  36. A Logic Of Sequences.Norihiro Kamide - 2011 - Reports on Mathematical Logic:29-57.
  37.  1
    Alternative Multilattice Logics: An Approach Based on Monosequent and Indexed Monosequent Calculi.Norihiro Kamide - forthcoming - Studia Logica:1-31.
    Two new multilattice logics called submultilattice logic and indexed multilattice logic are introduced as a monosequent calculus and an indexed monosequent calculus, respectively. The submultilattice logic is regarded as a monosequent calculus version of Shramko’s original multilattice logic, which is also known as the logic of logical multilattices. The indexed multilattice logic is an extension of the submultilattice logic, and is regarded as the logic of multilattices. A completeness theorem with respect to a lattice-valued semantics is proved for the submultilattice (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  38.  8
    Bounded Linear-Time Temporal Logic: A Proof-Theoretic Investigation.Norihiro Kamide - 2012 - Annals of Pure and Applied Logic 163 (4):439-466.
  39. Bunched Sequential Information.Norihiro Kamide - 2016 - Journal of Applied Logic 15:150-170.
  40. Cut-Elimination and Completeness in Dynamic Topological and Linear-Time Temporal Logics.Norihiro Kamide - 2011 - Logique Et Analyse 54 (215):379-394.
  41.  14
    Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic.Norihiro Kamide & Yoni Zohar - 2020 - Studia Logica 108 (3):549-571.
    In this study, we prove the completeness and cut-elimination theorems for a first-order extension F4CC of Arieli, Avron, and Zamansky’s ideal paraconsistent four-valued logic known as 4CC. These theorems are proved using Schütte’s method, which can simultaneously prove completeness and cut-elimination.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42. Combining Intuitionistic Logic with Paraconsistent Operators.Norihiro Kamide - 2012 - Logique Et Analyse 217:57-71.
  43.  5
    Classical Linear Logics with Mix Separation Principle.Norihiro Kamide - 2003 - Mathematical Logic Quarterly 49 (2):201-209.
    Variants of classical linear logics are presented based on the modal version of new structural rule !?mingle instead of the known rules !weakening and ?weakening. The cut-elimination theorems, the completeness theorems and a characteristic property named the mix separation principle are proved for these logics.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  44.  17
    Cut-Free Single-Succedent Systems Revisited.Norihiro Kamide - 2005 - Bulletin of the Section of Logic 34 (3):165-175.
    Direct download  
     
    Export citation  
     
    Bookmark  
  45.  4
    Correction to: Kripke-Completeness and Cut-elimination Theorems for Intuitionistic Paradefinite Logics With and Without Quasi-Explosion.Norihiro Kamide - 2020 - Journal of Philosophical Logic 49 (6):1213-1213.
    The original version of this article unfortunately contains several errors introduced by the typesetter during the publishing process. It has been corrected.
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  46.  27
    Extended Full Computation-Tree Logics for Paraconsistent Model Checking.Norihiro Kamide - 2007 - Logic and Logical Philosophy 15 (3):251-276.
    It is known that the full computation-tree logic CTL * is an important base logic for model checking. The bisimulation theorem for CTL* is known to be useful for abstraction in model checking. In this paper, the bisimulation theorems for two paraconsistent four-valued extensions 4CTL* and 4LCTL* of CTL* are shown, and a translation from 4CTL* into CTL* is presented. By using 4CTL* and 4LCTL*, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  47. Extended Full Computation-Tree Logics For Paraconsistent Model Checking.Norihiro Kamide - 2006 - Logic and Logical Philosophy 15:251-267.
    It is known that the full computation-tree logic CTL∗is an important base logic for model checking. The bisimulation theorem for CTL∗is known to be useful for abstraction in model checking. In this paper, thebisimulation theorems for two paraconsistent four-valued extensions 4CTL∗and 4LCTL∗of CTL∗are shown, and a translation from 4CTL∗into CTL∗ispresented. By using 4CTL∗and 4LCTL∗, inconsistency-tolerant and spatiotemporal reasoning can be expressed as a model checking framework.
     
    Export citation  
     
    Bookmark  
  48.  7
    Kripke-Completeness and Cut-elimination Theorems for Intuitionistic Paradefinite Logics With and Without Quasi-Explosion.Norihiro Kamide - 2020 - Journal of Philosophical Logic 49 (6):1185-1212.
    Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for (...)
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  49.  4
    Modal and Intuitionistic Variants of Extended Belnap–Dunn Logic with Classical Negation.Norihiro Kamide - forthcoming - Journal of Logic, Language and Information:1-41.
    In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  50.  9
    Modal Extension of Ideal Paraconsistent Four-Valued Logic and its Subsystem.Norihiro Kamide & Yoni Zohar - 2020 - Annals of Pure and Applied Logic 171 (10):102830.
    This study aims to introduce a modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC as a Gentzen-type sequent calculus and prove the Kripke-completeness and cut-elimination theorems for M4CC. The logic M4CC is also shown to be decidable and embeddable into the normal modal logic S4. Furthermore, a subsystem of M4CC, which has some characteristic properties that do not hold for M4CC, is introduced and the Kripke-completeness and cut-elimination theorems for this subsystem are proved. This subsystem (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 61