Katsuhiko Sano

The languages of logics based on team semantics typically only allow atomic negation or restricted negation. In this paper, we explore propositional team-based logics with full (intuitionistic) negation. We demonstrate that including full intuitionistic negation does not complicate the axiomatisation of propositional team-based logics with the downward closure property. We also review known expressive completeness results for these logics, highlighting how relevant complemented properties are expressed in propositional dependence logic without directly using negation. Building on these insights, we also prove a new result: propositional logic extended with both dependence and inclusion atoms is expressively complete.

The interpolation theorem of Craig is one of the most important results in formal logic. In the paper it is shown that it holds for elementary ontology of Leśniewski (LO), commonly regarded as the most comprehensive calculus of names. LO is a theoretical basis for mereology, an alternative foundation of mathematics, and can be also used as an efficient tool for direct formalisation of reasoning in natural languages. Showing that it satisfies interpolation increases its credibility of a well-behaved logical system. A cut-free analytic sequent calculus GO is used for this aim and a Maehara-style constructive proof of this result is provided.

In this paper, we discuss variations of K and S from the syntactical view of substructural logics without assuming both exchange and associativity. K and S are usually adopted as axioms on implication in Hilbert-style calculus for classical logic and intuitionistic logic. Particularly, K and S are related to weakening and contraction-like rules in sequent calculus LK and LJ. In substructural logics without the exchange rule, several variations of K and S can be considered because two types of implication exist. We present non-commutative and non-associative substructural logics with variations of K and S using Hilbert-style calculus and consider consecution calculus, which is a type of Gentzen-style calculus, algebraic semantics, the derivability of structural rules, such as contraction, exchange, and associativity, and the hierarchy.

The main goal of this paper is to introduce a novel method that allows us to construct systematically models of mereology. We call the resulting method mereological forcing. Whereas set-theoretic forcing deals with the construction of models which witness the compatibility of ZFC with certain set-theoretic statements, mereological forcing, is about the construction of models that establish the compatibility of a given mereological theory with certain mereological statements. Consequently, we claim that such a method constitutes a powerful tool for establishing compatibility claims for the mereologist. More concretely, we showcase this by constructing models which display the compatibility of (atomic) classical mereology with the mereological statement that expresses that their exist inconsistent objects.

This article argues that the thesis of composition as identity (CAI) is incoherent because its proponents assume the existence of composite objects (i.e., objects with proper parts) to propose the thesis to cast light on their nature. To do so, the article proves that CAI is logically equivalent to the (part-whole) triviality thesis, the thesis that everything is a part of itself but of nothing else. In proving this, the article distinguishes three formulations of CAI resulting from different analyses of the composition relation, and proves that all three formulations of the thesis are logically equivalent to the triviality thesis. It also argues that CAI is logically equivalent to the triviality thesis on any adequate analysis of composition.

The purpose of this paper is to investigate a variant of David Lewis’ imaging and to explore their relationship with conditionalization, a basic notion of belief change in Bayesianism, in terms of AGM-style postulates. This paper gives a formulation of conservative imaging restricting the selection function of possible worlds and its probabilistic postulates as an “intermediate” type of belief change in the sense that it has both the essential features of Lewis’ imaging and the significant property of conditionalization, namely, conservativity and compares it with types of them, including the clarification of non-trivial and immediate condition under which conditionalization and conservative imaging coincide within a certain convex combination.

We give a new generalization of Strict-tolerant logic. The main idea is that strict truth is the standard of truth accepted by everyone, and tolerant truth the standard accepted by someone. To formalize the idea, we use generalized matrices in abstract algebraic logic, defining strict truth as the intersection of the closure system in the given generalized matrix, and tolerant truth the union of it. We connect our generalized strict-tolerant logics with p-consequences and propose conditions for such logics to be classical. Compared to existing generalizations of Strict-tolerant logic, our generalization is both intuitive and general enough.

Hybrid logic is a modal logic with additional operators specifying nominals and is highly expressive. For example, there is no formula corresponding to the irreflexivity of Kripke frames in basic modal logic, but there is in hybrid logic. Irreflexivity is significant in that irreflexive and symmetric Kripke frames can be regarded as undirected graphs reviewed from a graph-theoretic point of view. Thus, the study of the hybrid logic with axioms corresponding to irreflexivity and symmetry can help to elucidate the logical properties of undirected graphs. In this paper, we formulate the tableau method of the hybrid logic for undirected graphs. Our main result is to show the completeness theorem and the termination property of the tableau method, which leads us to prove the decidability.

This book brings together contributions from philosophers interested in logic and logicians with a philosophical orientation to address a variety of logical and philosophical topics of current interest, including modal logic, intuitionistic logic, relevant logic, substructural logic, many-value logic, formal semantics, proof theory, and paradox. In particular, it provides the state of the art in three major aspects of current research in philosophical logic: negation, modality, and proof. New frameworks are proposed, e.g., meta sequent, unified inductive logic, generalized Clemens semantics, etc. The variety of topics and issues discussed in this volume is of interest to readers from a wide range of disciplines, such as logic, semantics, and computer science, philosophy, linguistics, artificial intelligence, and beyond.

This paper proposes cut-free sequent calculi for Wansing (1995)’s expansions of Nelson’s logics $$\textbf{N4}^{\bot }$$ (Odintsov 2005) and $$\textbf{N3}^{\bot }$$ with the consistency operator $${{\textsf{M}}}$$, which was originally studied in Gabbay (1982). A key semantic feature of the logics is the failure of the persistency condition in the Kripke semantics, and, as a result, the deduction theorem fails. Reflecting this aspect, we formulate the right rule for intuitionistic implication simi larly to the right rule for the strict implication for modal logic $$\textbf{S4}$$. Our calculus, with the cut rule, is sound, and its cut-free calculus is complete for the intended Kripke semantics. As a corollary, the cut-elimination theorem is established semantically. We also extract a Hilbert system from the sequent calculus. Unlike Omori (2016), we do not assume the existence of a root point in a Kripke model. Therefore, our Hilbert system is also semantically complete for the class of models that may lack the root point.

This paper proposes non-labelled sequent calculi, G(K45PAL) and G(SK5PAL), for the public announcement expansions of modal logics K45 and S5. We transform each of the recursion axioms of PAL into left and right rules for the sequent calculi. For G(K45PAL), the cut elimination theorem is shown using the complexity measure introduced by van Ditmarsch et al. (2007). This measure was originally employed to establish semantic completeness via recursion axioms. While the cut elimination theorem fails in G(SK5PAL), we adopt Takano’s strategy (1992) to establish that the cut formula in G(SK5PAL) can be restricted to the set of suitably extended subformulas (i.e., closure) of the conclusion of the cut rule.

The logic of the hide and seek game $$\textbf{LHS}$$ was proposed to capture interactions between agents in pursuit-evasion environments. In this paper, we explore a hybrid extension of $$\textbf{LHS}$$ and show that such an extension is beneficial in several aspects. We will show that it improves the technical properties of the resulting logical system, and expands the potential applications of the system. Specifically, we will investigate the expressive power of the hybrid logic of the hide and seek game $${\mathcal {H}}(\textbf{LHS})$$ and its crucial fragment $${\mathcal {H}}(\textbf{LHS}^{-})$$, at both model and frame levels. We will present complete Hilbert-style proof systems for both the logics $${\mathcal {H}}(\textbf{LHS}^{-})$$ and $${\mathcal {H}}(\textbf{LHS})$$, which in fact provides a solution to a known open problem.

This paper studies a combined system of intuitionistic and classical propositional logic from proof-theoretic viewpoints. Based on the semantic treatment of Humberstone (J Philos Log 8:171–196, 1979) and del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996), a sequent calculus \(\textsf{G}(\textbf{C}+\textbf{J})\) is proposed. An approximate idea of obtaining \(\textsf{G}(\textbf{C}+\textbf{J})\) is adding rules for classical implication on top of the intuitionistic multi-succedent sequent calculus by Maehara (Nagoya Math J 7:45–64, 1954). However, in the semantic treatment, some formulas do not satisfy heredity, which leads to the necessity of a restriction on the right rule for intuitionistic implication to keep the soundness of the calculus. The calculus \(\textsf{G}(\textbf{C}+\textbf{J})\) enjoys cut elimination and Craig interpolation, whose detailed proofs are described in this paper. Cut elimination enables us to show the decidability of this combination both directly and syntactically. This paper also employs a canonical model argument to establish the strong completeness of Hilbert system \(\mathbf {C+J}\) proposed by del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996).

This paper shows Hilbert system (C+J)-, given by del Cerro and Herzig (1996) is semantically incomplete. This system is proposed as a proof theory for Kripke semantics for a combination of intuitionistic and classical propositional logic, which is obtained by adding the natural semantic clause of classical implication into intuitionistic Kripke semantics. Although Hilbert system (C+J)- contains intuitionistic modus ponens as a rule, it does not contain classical modus ponens. This paper gives an argument ensuring that the system (C+J)- is semantically incomplete because of the absence of classical modus ponens. Our method is based on the logic of paradox, which is a paraconsistent logic proposed by Priest (1979).

We develop intuitionistic public announcement logic over intuitionistic \({\textbf{K}}\), \({{\textbf{K}}}{{\textbf{T}}}\), \({{\textbf{K}}}{{\textbf{4}}}\), and \({{\textbf{S}}}{{\textbf{4}}}\) with distributed knowledge. We reveal that a recursion axiom for the distributed knowledge is _not_ valid for a frame class discussed in [ 12 ] but valid for the restricted frame class introduced in [ 20, 26 ]. The semantic completeness of the static logics for this restricted frame class is established via the concept of pseudo-model.

Artemov and Protopopescu introduced a Brouwer-Heyting-Kolmogorov interpretation of knowledge operator to define the intuitionistic epistemic logic IEL, where the axiom $$A\supset KA$$ is accepted but the axiom $$KA\supset A$$ is refused. This paper studies the notion of distributed knowledge on an expansion of the multi agent variant of IEL. We provide a BHK interpretation of distributed knowledge operator to define the intuitionistic epistemic logic with distributed knowledge DIEL. We construct Hilbert system and cut-free sequent calculus for $$\mathbf {DIEL}$$ and show that they are sound and complete for the intended Kripke semantics.

Intuitionistic epistemic logic by Artemov and Protopopescu (Rev Symb Log 9:266–298, 2016) accepts the axiom “if A, then A is known” (written $$A \supset K A$$ ) in terms of the Brouwer–Heyting–Kolmogorov interpretation. There are two variants of intuitionistic epistemic logic: one with the axiom “ $$KA \supset \lnot \lnot A$$ ” and one without it. The former is called $$\textbf{IEL}$$, and the latter is called $$\textbf{IEL}^{-}$$. The aim of this paper is to study first-order expansions (with equality and function symbols) of these two intuitionistic epistemic logics. We define Hilbert systems with additional axioms called geometric axioms and sequent calculi with the corresponding rules to geometric axioms and prove that they are sound and complete for the intended semantics. We also prove the cut-elimination theorems for both sequent calculi. As a consequence, the disjunction property and existence property are established for the sequent calculi without geometric implications. Finally, we establish that our sequent calculi can also be formulated with admissible structural rules (i.e., in terms of a G3-style sequent calculus).

One of the problems we face in many-valued logic is the difficulty of capturing the intuitive meaning of the connectives introduced through truth tables. At the same time, however, some logics have nice ways to capture the intended meaning of connectives easily, such as four-valued logic studied by Belnap and Dunn. Inspired by Dunn’s discovery, we first describe a mechanical procedure, in expansions of Belnap-Dunn logic, to obtain truth conditions in terms of the behavior of the Truth and the False, which gives us intuitive readings of connectives, out of truth tables. Then, we revisit the notion of functional completeness, which is one of the key notions in many-valued logic, in view of Dunn’s idea. More concretely, we introduce a generalized notion of functional completeness which naturally arises in the spirit of Dunn’s idea, and prove some fundamental results corresponding to the classical results proved by Post and Słupecki

The present contribution shows that a Hilbert-style axiomatization for dynamic logic of relation changers is complete for the standard Kripke semantics not by a well-known rewriting technique but by the idea of an auxiliary semantics studied by van Benthem and Wang et al. A key insight of our auxiliary semantics for dynamic logic of relation changers can be described as: “relation changers are bounded morphisms.” Moreover, we demonstrate that this semantic insight can be used to provide a modular cut-free labelled sequent calculus for the logic in the sense that our calculus can be regarded as a natural expansion of a labelled sequent calculus of iteration-free propositional dynamic logic.