Abstract Dynamic epistemic logic is a logic that is aimed at formally expressing how a person’s knowledge changes. We provide a cut-free labelled sequent calculus ($\textbf{GDEL}$) on the background of existing studies of Hilbert-style axiomatization $\textbf{HDEL}$ of dynamic epistemic logic and labelled calculi for public announcement logic. We first show that the $cut$ rule is admissible in $\textbf{GDEL}$ and show that $\textbf{GDEL}$ is sound and complete for Kripke semantics. Moreover, we show that the basis of $\textbf{GDEL}$ is extended from modal logic K to other familiar modal logics including S5 with keeping the admissibility of cut, soundness and completeness.

versions of selected contributions presented at the 16th Workshop on Logic, Language, Information and Computation (WoLLIC 2009), held from June 21 through 24, 2009, in the National Center of Sciences, Tokyo, Japan.WoLLIC is a series of workshops which started in 1994 with the aim of fostering interdisciplinary research in pure and applied logic.The idea of the workshop is to have a forum which is large enough in the number of possible interactions between logic and the sciences related to information and computation, and yet is small enough to allow for concrete and useful interaction across logic-related disciplines.Held over the course of four full days, WoLLIC 2009 included both extended tutorial sessions and general lectures, given by an international panel of the world's top experts in the fields of theoretical and applied logic, linguistics, and computer science.The composition of the speakers and the other participants of the workshop reflected the diversity of the event: included were members of psycholinguistics, cognitive science, mathematics, philosophy, theoretical computer science and business software communities from geographical locales as close to home as Tokyo, to as far away places such as Brazil and Iran.The close contact between the speakers and the other participants ensued, within the intensive workshop environment, an intimate setting in which the free and fruitful exchange of ideas could take place.

Journal Article Interpolation Properties, Beth Definability Properties and Amalgamation Properties for Substructural Logics Get access Hitoshi Kihara, Hitoshi Kihara School of Information Science, Japan Advanced Institute of Science and Technology, Asahidai, Nomi, Ishikawa, 923-1292, Japan.E-mail: [email protected]; [email protected] Search for other works by this author on: Oxford Academic Google Scholar Hiroakira Ono Hiroakira Ono School of Information Science, Japan Advanced Institute of Science and Technology, Asahidai, Nomi, Ishikawa, 923-1292, Japan.E-mail: [email protected]; [email protected] Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 20, Issue 4, August 2010, Pages 823–875, https://doi.org/10.1093/logcom/exn084 Published: 08 January 2009 Article history Received: 20 January 2008 Published: 08 January 2009

Abstract It is well known that classical propositional logic can be interpreted in intuitionistic prepositional logic. In particular Glivenko's theorem states that a formula is provable in the former iff its double negation is provable in the latter. We extend Glivenko's theorem and show that for every involutive substructural logic there exists a minimum substructural logic that contains the first via a double negation interpretation. Our presentation is algebraic and is formulated in the context of residuated lattices. In the last part of the paper, we also discuss some extended forms of the Koltnogorov translation and we compare it to the Glivenko translation.

Abstract For each ordinal α > 0, L(α) is the intermediate predicate logic characterized by the class of all Kripke frames with the poset α and with constant domain. This paper will be devoted to a study of logics of the form L(α). It will be shown that for each uncountable ordinal of the form α + η with a finite or a countable η(> 0), there exists a countable ordinal of the form β + η such that L(α + η) = L(β + η). On the other hand, such a reduction of ordinals to countable ones is impossible for a logic L(α) if α is an uncountable regular ordinal. Moreover, it will be proved that the mapping L is injective if it is restricted to ordinals less than ωω, i.e. α ≠ β implies L(α) ≠ L(β) for each ordinal α, β ≤ ωω.

We will study syntactical and semantical properties of propositional logics weaker than the intuitionistic, in which the contraction rule (or, the exchange rule or the weakening rule, in some cases) does not hold. Here, the contraction rule means the rule of inference of the form if we formulate our logics in a Gentzen-type formal system. Some syntactical properties of these logics have been studied firstly by the second author in [11], in connection with the study of BCK-algebras (for information on BCK-algebras, see [9]). There, it turned out that such a syntactical method is a powerful and promising tool in studying BCK-algebras. Using this method, considerable progress has been made since then (see, e.g., [8], [18], [27]). In this paper, we will study these logics more comprehensively. We notice here that the distributive law does not hold necessarily in these logics. By adding some axioms (or initial sequents) and rules of inference to these basic logics, we can obtain a lot of interesting nonclassical logics such as Łukasiewicz's many-valued logics, relevant logics, the intuitionistic logic and logics related to BCK-algebras, which have been studied separately until now. Thus, our approach will give a uniform way of dealing with these logics. One of our two main tools in doing so is Gentzen-type formulation of logics in syntax, and the other is semantics defined by using partially ordered monoids.