Citations of:
Add citations
You must login to add citations.


We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2variable fragment of firstorder logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into firstorder logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) 



In this paper we provide frame definability results for weak versions of classical modal axioms that can be expressed in Fitting's manyvalued modal languages. These languages were introduced by M. Fitting in the early '90s and are built on Heyting algebras which serve as the space of truth values. The possibleworlds frames interpreting these languages are directed graphs whose edges are labelled with an element of the underlying Heyting algebra, providing us a form of manyvalued accessibility relation. Weak axioms of (...) 

Propositional logic is understood as a set of theorems defined by a deductive system: a set of axioms and a set of rules. Superintuitionistic logic is a logic extending intuitionistic propositional logic \. A rule is admissible for a logic if any substitution that makes each premise a theorem, makes the conclusion a theorem too. A deductive system \ is structurally complete if any rule admissible for the logic defined by \ is derivable in \. It is known that any (...) 

Hamkins and Löwe proved that the modal logic of forcing is S4.2 . In this paper, we consider its modal companion, the intermediate logic KC and relate it to the fatal Heyting algebra H ZFC of forcing persistent sentences. This Heyting algebra is equationally generic for the class of fatal Heyting algebras. Motivated by these results, we further analyse the class of fatal Heyting algebras. 

By a wellknown result of Cook and Reckhow [S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journal of Symbolic Logic 44 36–50; R.A. Reckhow, On the lengths of proofs in the propositional calculus, Ph.D. Thesis, Department of Computer Science, University of Toronto, 1976], all Frege systems for the classical propositional calculus are polynomially equivalent. Mints and Kojevnikov [G. Mints, A. Kojevnikov, Intuitionistic Frege systems are polynomially equivalent, Zapiski Nauchnyh Seminarov POMI 316 129–146] have recently shown pequivalence of (...) 

If □ is conceived as an operator, i.e., an expression that gives applied to a formula another formula, the expressive power of the language is severely restricted when compared to a language where □ is conceived as a predicate, i.e., an expression that yields a formula if it is applied to a term. This consideration favours the predicate approach. The predicate view, however, is threatened mainly by two problems: Some obvious predicate systems are inconsistent, and possibleworlds semantics for predicates of (...) 

Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilberttype system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that (...) 

Only propositional logics are at issue here. Such a logic is contraclassical in a superficial sense if it is not a sublogic of classical logic, and in a deeper sense, if there is no way of translating its connectives, the result of which translation gives a sublogic of classical logic. After some motivating examples, we investigate the incidence of contraclassicality (in the deeper sense) in various logical frameworks. In Sections 3 and 4 we will encounter, originally as an example of (...) 

In a previous work we introduced the algorithm \SQEMA\ for computing firstorder equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...) 

In the paper we consider complexity of intuitionistic propositional logic and its natural fragments such as implicative fragment, finitevariable fragments, and some others. Most facts we mention here are known and obtained by logicians from different countries and in different time since 1920s; we present these results together to see the whole picture. 

In this paper we study natural deduction for the intuitionistic and classical modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multicontextual structure, called Tsequent, that allows to design simple labelfree natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the subformula property in the intuitionistic case. 

We introduce a bimodal epistemic logic intended to capture knowledge as truth in all epistemically alternative states and belief as a generalised ‘majority’ quantifier, interpreted as truth in most of the epistemically alternative states. This doxastic interpretation is of interest in knowledgerepresentation applications and it also holds an independent philosophical and technical appeal. The logic comprises an epistemic modal operator, a doxastic modal operator of consistent and complete belief and ‘bridge’ axioms which relate knowledge to belief. To capture the notion (...) 

Trying to overcome Dugundji’s result on uncharacterisability of modal logics by finite logical matrices, Kearns and Ivlev proposed, independently, a characterisation of some modal systems by means of fourvalued multivalued truthfunctions , as an alternative to Kripke semantics. This constitutes an antecedent of the nondeterministic matrices introduced by Avron and Lev . In this paper we propose a reconstruction of Kearns’s and Ivlev’s results in a uniform way, obtaining an extension to another modal systems. The first part of the paper (...) 

It is natural to ask under what conditions negating a conditional is equivalent to negating its consequent. Given a bivalent background logic, this is equivalent to asking about the conjunction of Conditional Excluded Middle and Weak Boethius' Thesis. In the system CI.0 of consequential implication, which is intertranslatable with the modal logic KT, WBT is a theorem, so it is natural to ask which instances of CEM are derivable. We also investigate the systems CIw and CI of consequential implication, corresponding (...) 

This work treats the problem of axiomatizing the truth and falsity consequence relations, $ \vDash _t $ and $ \vDash _f $, determined via truth and falsity orderings on the trilattice SIXTEEN₃. The approach is based on a representation of SIXTEEN₃ as a twiststructure over the twoelement Boolean algebra. 

The paper is a brief survey of the most important semantic constructions founded on the concept of possible world. It is impossible to capture in one short paper the whole variety of the problems connected with manifold applications of possible worlds. Hence, after a brief explanation of some philosophical matters I take a look at possible worlds from rather technical standpoint of logic and focus on the applications in formal semantics. In particular, I would like to focus on the fruitful (...) 

Earlier algebraic semantics for Belnapian modal logics were defined in terms of twiststructures over modal algebras. In this paper we introduce the class of BK lattices, show that this class coincides with the abstract closure of the class of twiststructures, and it forms a variety. We prove that the lattice of subvarieties of the variety of BK lattices is dually isomorphic to the lattice of extensions of Belnapian modal logic BK . Finally, we describe invariants determining a twiststructure over a (...) 

A logic is called metacomplete if formulas that are true in a certain preferred interpretation of that logic are theorems in its metalogic. In the area of relevant logics, metacompleteness is used to prove primeness, consistency, the admissibility of γ and so on. This paper discusses metacompleteness and its applications to a wider class of modal logics based on contractionless relevant logics and their neighbours using Slaney’s metavaluational technique. 

This paper partly answers the question “what a frame may be exactly like when it characterizes a pretabular logic in NExtK4”. We prove the pretabularity crieria for the logics of finite depth in NExtK4. In order to find out the criteria, we create two useful concepts—“pointwise reduction” and “invariance under pointwise reductions”, which will remain important in dealing with the case of infinite depth. 

The trilattice SIXTEEN₃ is a natural generalization of the wellknown bilattice FOUR₂. Cutfree, sound and complete sequent calculi for truth entailment and falsity entailment in SIXTEEN₃, are presented. 

The point of the present paper is to draw attention to some interesting similarities, as well as differences, between the approaches to the logic of noncontingency of Evgeni Zolin and of Claudio Pizzi. Though neither of them refers to the work of the other, each is concerned with the definability of a (normally behaving, though not in general truthimplying) notion of necessity in terms of noncontingency, standard boolean connectives and additional but nonmodal expressive resources. The notion of definability involved is (...) 

Using labelled formulae, a cutfree sequent calculus for intuitionistic propositional logic is presented, together with an easy cutadmissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive prooftheoretic methods, without appeal to semantics other than in the (...) 

Skvortsova showed that there is a factor of the Medvedev lattice which captures intuitionistic propositional logic. However, her factor is unnatural in the sense that it is constructed in an ad hoc manner. We present a more natural example of such a factor. We also show that the theory of every nontrivial factor of the Medvedev lattice is contained in Jankov’s logic, the deductive closure of IPC plus the weak law of the excluded middle ¬p∨¬¬p\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} (...) 

All extensions of the modal Grzegorczyk logic Grz possessing projective Beth's property PB2 are described. It is proved that there are exactly 13 logics over Grz with PB2. All of them are finitely axiomatizable and have the finite model property. It is shown that PB2 is strongly decidable over Grz, i.e. there is an algorithm which, for any finite system Rul of additional axiom schemes and rules of inference, decides if the calculus Grz+Rul has the projective Beth property. 

The modal logic of Gödel sentences, termed as GS, is introduced to analyze the logical properties of 'true but unprovable' sentences in formal arithmetic. The logic GS is, in a sense, dual to Grzegorczyk's Logic, where modality can be interpreted as 'true and provable'. As we show, GS and Grzegorczyk's Logic are, in fact, mutually embeddable. We prove Kripke completeness and arithmetical completeness for GS. GS is also an extended system of the logic of 'Essence and Accident' proposed by Marcos (...) 

This work treats the problem of axiomatizing the truth and falsity consequence relations, $ \vDash _t $ and $ \vDash _f $, determined via truth and falsity orderings on the trilattice SIXTEEN₃. The approach is based on a representation of SIXTEEN₃ as a twiststructure over the twoelement Boolean algebra. 

We prove strong completeness of the □version and the ◊version of a Gödel modal logic based on Kripke models where propositions at each world and the accessibility relation are both infinitely valued in the standard Gödel algebra [0,1]. Some asymmetries are revealed: validity in the first logic is reducible to the class of frames having twovalued accessibility relation and this logic does not enjoy the finite model property, while validity in the second logic requires truly fuzzy accessibility relations and this (...) 

In this paper we give an example of intertranslatability between an ontology of individuals (nominalism), an ontology of properties (realism), and an ontology of facts (factualism). We demonstrate that these three ontologies are dual to each other, meaning that each ontology can be translated into, and recaptured from, each of the others. The aiin of the enterprise is to raise the possibility that, at least in some settings, there may be no need for considerations of ontological primacy. Whether the world (...) 

Monomodal logic has exactly two maximally normal logics, which are also the only quasinormal logics that are Post complete, and they are complete for validity in Kripke frames. Here we show that addition of a propositional constant to monomodal logic allows the construction of continuum many maximally normal logics that are not valid in any Kripke frame, or even in any complete modal algebra. We also construct continuum many quasinormal Post complete logics that are not normal. The set of extensions (...) 

This paper investigates a generalized version of inquisitive semantics. A complete axiomatization of the associated logic is established, the connection with intuitionistic logic and several intermediate logics is explored, and the generalized version of inquisitive semantics is argued to have certain advantages over the system that was originally proposed by Groenendijk (2009) and Mascarenhas (2009). 

By introducing the intensional mappings and their properties, we establish a new semantical approach of characterizing intermediate logics. First prove that this new approach provides a general method of characterizing and comparing logics without changing the semantical interpretation of implication connective. Then show that it is adequate to characterize all Kripke_complete intermediate logics by showing that each of these logics is sound and complete with respect to its (unique) ‘weakest characterization property’ of intensional mappings. In particular, we show that classical (...) 

Standard models for model predicate logic consist of a Kripke frame whose worlds come equipped with relational structures. Both modal and twosorted predicate logic are natural languages for speaking about such models. In this paper we compare their expressivity. We determine a fragment of the twosorted language for which the modal language is expressively complete on S5models. Decidable criteria for modal definability are presented. 

Algebraic approach to study of classical and nonclassical logical calculi was developed and systematically presented by Helena Rasiowa in [48], [47]. It is very fruitful in investigation of nonclassical logics because it makes possible to study large families of logics in an uniform way. In such research one can replace logics with suitable classes of algebras and apply powerful machinery of universal algebra. In this paper we present an overview of results on interpolation and definability in modal and positive logics,and (...) 

We consider two topological interpretations of the modal diamond—as the closure operator (Csemantics) and as the derived set operator (dsemantics). We call the logics arising from these interpretations Clogics and dlogics, respectively. We axiomatize a number of subclasses of the class of nodec spaces with respect to both semantics, and characterize exactly which of these classes are modally definable. It is demonstrated that the dsemantics is more expressive than the Csemantics. In particular, we show that the dlogics of the six (...) 

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property. 

JeanYves Béziau (‘Classical Negation can be Expressed by One of its Halves’, Logic Journal of the IGPL 7 (1999), 145–151) has given an especially clear example of a phenomenon he considers a sufficiently puzzling to call the ‘paradox of translation’: the existence of pairs of logics, one logic being strictly weaker than another and yet such that the stronger logic can be embedded within it under a faithful translation. We elaborate on Béziau’s example, which concerns classical negation, as well as (...) 

Since 1993, when Hudelmaier developed an Ospace decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proofsearch algorithms. In this paper a tableau calculus using the signs T, F and F c with a new set of rules to treat signed formulas of the kind T → C) is provided. The main feature of the calculus is the reduction of both the nondeterminism in proofsearch and the width of proofs (...) 

We establish the dichotomy property for stable canonical multiconclusion rules for IPC, K4, and S4. This yields an alternative proof of existence of explicit bases of admissible rules for these logics. 

Kolmogorov introduced an informal calculus of problems in an attempt to provide a classical semantics for intuitionistic logic. This was later formalised by Medvedev and Muchnik as what has come to be called the Medvedev and Muchnik lattices. However, they only formalised this for propositional logic, while Kolmogorov also discussed the universal quantifier. We extend the work of Medvedev to firstorder logic, using the notion of a firstorder hyperdoctrine from categorical logic, to a structure which we will call the hyperdoctrine (...) 

In this paper we study the expressive power and definability for modal languages interpreted on topological spaces. We provide topological analogues of the van Benthem characterization theorem and the Goldblatt–Thomason definability theorem in terms of the wellestablished firstorder topological language. 

We introduce partial Esakia morphisms, well partial Esakia morphisms, and strong partial Esakia morphisms between Esakia spaces and show that they provide the dual description of homomorphisms, homomorphisms, and homomorphisms between Heyting algebras, thus establishing a generalization of Esakia duality. This yields an algebraic characterization of Zakharyaschev’s subreductions, cofinal subreductions, dense subreductions, and the closed domain condition. As a consequence, we obtain a new simplified proof of Zakharyaschev’s theorem that each intermediate logic can be axiomatized by canonical formulas. 

We show that if we interpret modal diamond as the derived set operator of a topological space, then the modal logic of Stone spaces is _K4_ and the modal logic of weakly scattered Stone spaces is _K4G_. As a corollary, we obtain that _K4_ is also the modal logic of compact Hausdorff spaces and _K4G_ is the modal logic of weakly scattered compact Hausdorff spaces. 

The literature on quantum logic emphasizes that the algebraic structures involved with orthodox quantum mechanics are non distributive. In this paper we develop a particular algebraic structure, the quasilattice (Jlattice), which can be modeled by an algebraic structure built in quasiset theory Q. This structure is non distributive and involve indiscernible elements. Thus we show that in taking into account indiscernibility as a primitive concept, the quasilattice that 'naturally' arises is non distributive. 

The aim of this paper is to give new kinds of modal logics suitable for reasoning about regions in discrete spaces. We call them dynamic logics of the regionbased theory of discrete spaces. These modal logics are linguistic restrictions of propositional dynamic logic with the global diamond E. Their formulas are equivalent to Boolean combinations of modal formulas like E where A and B are Boolean terms and α is a relational term. Examining what we can say about dynamic models (...) 

The Local Computation Framework has been used to improve the efficiency of computation in various uncertainty formalisms. This paper shows how the framework can be used for the computation of logical deduction in two different ways; the first way involves embedding model structures in the framework; the second, and more direct, way involves embedding sets of formulae. This work can be applied to many of the logics developed for different kinds of reasoning, including predicate calculus, modal logics, possibilistic logics, probabilistic (...) 

In his 1964 note, ‘Two Additions to Positive Implication’, A. N. Prior showed that standard axioms governing conjunction yield a nonconservative extension of the pure implicational intermediate logic OIC of R. A. Bull. Here, after reviewing the situation with the aid of an adapted form of the Kripke semantics for intuitionistic and intermediate logics, we proceed to illuminate this example by transposing it to the setting of modal logic, and then relate it to the propositional logic of what have been (...) 

ABSTRACT The paper studies propositional logics in a bimodal language, in which the first modality is interpreted as the local truth, and the second as the universal truth. The logic S4UC is introduced, which is finitely axiomatizable, has the f.m.p. and is determined by every connected separable metric space. 

We assemble material from the literature on matrix methodology for sentential logic?without claiming to present any new logical results?in order to show that Gödel once made (or at least, is quoted as having made) an uncharacteristically illconsidered remark in this area. 