scholarly journals Remarks about the unification type of several non-symmetric non-transitive modal logics

2018 ◽  
Vol 27 (5) ◽  
pp. 639-658 ◽  
Author(s):  
Philippe Balbiani

Abstract The problem of unification in a normal modal logic $L$ can be defined as follows: given a formula $\varphi$, determine whether there exists a substitution $\sigma$ such that $\sigma (\varphi )$ is in $L$. In this paper, we prove that for several non-symmetric non-transitive modal logics, there exists unifiable formulas that possess no minimal complete set of unifiers.

2018 ◽  
Vol 11 (3) ◽  
pp. 436-469 ◽  
Author(s):  
GURAM BEZHANISHVILI ◽  
NICK BEZHANISHVILI ◽  
JULIA ILIN

AbstractStable logics are modal logics characterized by a class of frames closed under relation preserving images. These logics admit all filtrations. Since many basic modal systems such as K4 and S4 are not stable, we introduce the more general concept of an M-stable logic, where M is an arbitrary normal modal logic that admits some filtration. Of course, M can be chosen to be K4 or S4. We give several characterizations of M-stable logics. We prove that there are continuum many S4-stable logics and continuum many K4-stable logics between K4 and S4. We axiomatize K4-stable and S4-stable logics by means of stable formulas and discuss the connection between S4-stable logics and stable superintuitionistic logics. We conclude the article with many examples (and nonexamples) of stable, K4-stable, and S4-stable logics and provide their axiomatization in terms of stable rules and formulas.


2019 ◽  
Vol 13 (2) ◽  
pp. 416-435 ◽  
Author(s):  
SERGEI P. ODINTSOV ◽  
STANISLAV O. SPERANSKI

AbstractWe shall be concerned with the modal logic BK—which is based on the Belnap–Dunn four-valued matrix, and can be viewed as being obtained from the least normal modal logic K by adding ‘strong negation’. Though all four values ‘truth’, ‘falsity’, ‘neither’ and ‘both’ are employed in its Kripke semantics, only the first two are expressible as terms. We show that expanding the original language of BK to include constants for ‘neither’ or/and ‘both’ leads to quite unexpected results. To be more precise, adding one of these constants has the effect of eliminating the respective value at the level of BK-extensions. In particular, if one adds both of these, then the corresponding lattice of extensions turns out to be isomorphic to that of ordinary normal modal logics.


2019 ◽  
pp. 149-161
Author(s):  
Luciano Floridi

In this chapter, the principle of information closure (PIC) is defined and defended against a sceptical objection similar to the one discussed by Dretske in relation to the principle of epistemic closure. If successful, given that PIC is equivalent to the axiom of distribution and that the latter is one of the conditions that discriminate between normal and non-normal modal logics, one potentially good reason to look for a formalization of the logic of ‘S is informed that p’ among the non-normal modal logics, which reject the axiom, is also removed. This is not to argue that the logic of ‘S is informed that p’ should be a normal modal logic, but that it could still be, insofar as the objection that it could not be, based on the sceptical objection against PIC, has been removed. In other words, this chapter argues that the sceptical objection against PIC fails, so such an objection provides no ground to abandon the normal modal logic B (also known as KTB) as a formalization of ‘S is informed that p’, which remains plausible insofar as this specific obstacle is concerned.


10.29007/jsb9 ◽  
2018 ◽  
Author(s):  
Tobias Gleißner ◽  
Alexander Steen ◽  
Christoph Benzmüller

We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used as a preprocessor for turning TPTP THF-compliant the- orem provers into provers for various modal logics. The choice of the concrete modal logic is thereby specified within the problem as a meta-logical statement. This specification for- mat as well as the underlying semantics parameters are discussed, and the implementation and the operation of the tool are outlined.By combining our tool with one or more THF-compliant theorem provers we accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other available prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive, at least for quantified modal logics, as our experiments demonstrate.


1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani

The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.


10.29007/hgbj ◽  
2018 ◽  
Author(s):  
Nick Bezhanishvili

The method of canonical formulas is a powerful tool for investigating intuitionistic and modal logics. In this talk I will discuss an algebraic approach to this method. I will mostly concentrate on the case of intuitionistic logic. But I will also review the case of modal logic and possible generalizations to substructural logic.


2019 ◽  
Vol 13 (4) ◽  
pp. 720-747
Author(s):  
SERGEY DROBYSHEVICH ◽  
HEINRICH WANSING

AbstractWe present novel proof systems for various FDE-based modal logics. Among the systems considered are a number of Belnapian modal logics introduced in Odintsov & Wansing (2010) and Odintsov & Wansing (2017), as well as the modal logic KN4 with strong implication introduced in Goble (2006). In particular, we provide a Hilbert-style axiom system for the logic $BK^{\square - } $ and characterize the logic BK as an axiomatic extension of the system $BK^{FS} $. For KN4 we provide both an FDE-style axiom system and a decidable sequent calculus for which a contraction elimination and a cut elimination result are shown.


2014 ◽  
Vol 8 (1) ◽  
pp. 178-191 ◽  
Author(s):  
GURAM BEZHANISHVILI ◽  
DAVID GABELAIA ◽  
JOEL LUCERO-BRYAN

AbstractIt is a classic result (McKinsey & Tarski, 1944; Rasiowa & Sikorski, 1963) that if we interpret modal diamond as topological closure, then the modal logic of any dense-in-itself metric space is the well-known modal system S4. In this paper, as a natural follow-up, we study the modal logic of an arbitrary metric space. Our main result establishes that modal logics arising from metric spaces form the following chain which is order-isomorphic (with respect to the ⊃ relation) to the ordinal ω + 3:$S4.Gr{z_1} \supset S4.Gr{z_2} \supset S4.Gr{z_3} \supset \cdots \,S4.Grz \supset S4.1 \supset S4.$It follows that the modal logic of an arbitrary metric space is finitely axiomatizable, has the finite model property, and hence is decidable.


1999 ◽  
Vol 64 (1) ◽  
pp. 99-138 ◽  
Author(s):  
Marcus Kracht ◽  
Frank Wolter

AbstractThis paper shows that non-normal modal logics can be simulated by certain polymodal normal logics and that polymodal normal logics can be simulated by monomodal (normal) logics. Many properties of logics are shown to be reflected and preserved by such simulations. As a consequence many old and new results in modal logic can be derived in a straightforward way, sheding new light on the power of normal monomodal logic.


Sign in / Sign up

Export Citation Format

Share Document