ON SOME INTERPRETATIONS OF CLASSICAL LOGIC

In distinction from the well-known double-negation embeddings of the classical logic we consider some variants of single-negation embeddings and describe some classes of superintuitionistic first-order predicate logics in which the classical first-order calculus is interpretable in such a way. Also we find the minimal extensions of Heyting's logic in which the classical predicate logic can be embedded by means of these translations.     

On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics.     

All Finitely Axiomatizable Normal Extensions of K4.3 are Decidable

We use the apparatus of the canonical formulas introduced by Zakharyaschev [10] to prove that all finitely axiomatizable normal modal logics containing K4.3 are decidable, though possibly not characterized by classes of finite frames. Our method is purely frame-theoretic. Roughly, given a normal logic L above K4.3, we enumerate effectively a class of (possibly infinite) frames with respect to which L is complete, show how to check effectively whether a frame in the class validates a given formula, and then apply a Harropstyle argument to establish the decidability of L, provided of course that it has finitely many axioms.     

Modal characterisation theorems over special classes of frames

We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem’s theorem, which says that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes-for instance, rooted frames, finite rooted frames, finite transitive frames, well-founded transitive frames, finite equivalence frames-as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraïssé versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes. Over most of the classes considered, we obtain finite model theory analogues of the classically expected characterisations, with new proofs also for the classical setting. The class of transitive frames is a notable exception, with a marked difference between the classical and the finite model theory of bisimulation invariant first-order properties. Over the class of all finite transitive frames in particular, we find that monadic second-order logic is no more expressive than first-order as far as bisimulation invariant properties are concerned — though both are more expressive here than basic modal logic. We obtain ramifications of the de Jongh-Sambin theorem and a new and specific analogue of the Janin-Walukiewicz characterisation of bisimulation invariant monadic second-order for finite transitive frames.     

On non‐compact logics in NEXT(KTB)

In this paper we construct a continuum of logics, extensions of the modal logic T₂ = KTB ⊕ □²p → □³p, which are non‐compact (relative to Kripke frames) and hence Kripke incomplete. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The Skolemization of prenex formulas in intermediate logics

The skolem class of a logic consists of the formulas for which the derivability of the formula is equivalent to the derivability of its Skolemization. In contrast to classical logic, the skolem classes of many intermediate logics do not contain all formulas. In this paper it is proven for certain classes of propositional formulas that any instance of them by (independent) predicate sentences in prenex normal form belongs to the skolem class of any intermediate logic complete with respect to a class of well-founded trees. In particular, all prenex sentences belong to the skolem class of these logics, and this result extends to the constant domain versions of these logics.     

Two Semantical Approaches to Paraconsistent Modalities

In this paper we extend the anodic systems introduced in Bueno-Soler (J Appl Non Class Logics 19(3):291–310, 2009) by adding certain paraconsistent axioms based on the so called logics of formal inconsistency, introduced in Carnielli et al. (Handbook of philosophical logic, Springer, Amsterdam, 2007), and define the classes of systems that we call cathodic. These classes consist of modal paraconsistent systems, an approach which permits us to treat with certain kinds of conflicting situations. Our interest in this paper is to show that such systems can be semantically characterized in two different ways: by Kripke-style semantics and by modal possible-translations semantics. Such results are inspired in some universal constructions in logic, in the sense that cathodic systems can be seen as a kind of fusion (a particular case of fibring) between modal logics and non-modal logics, as discussed in Carnielli et al. (Analysis and synthesis of logics, Springer, Amsterdam, 2007). The outcome is inherently within the spirit of universal logic, as our systems semantically intermingles modal logics, paraconsistent logics and many-valued logics, defining new blends of logics whose relevance we intend to show.     

A Sahlqvist theorem for distributive modal logic

In this paper we consider distributive modal logic, a setting in which we may add modalities, such as classical types of modalities as well as weak forms of negation, to the fragment of classical propositional logic given by conjunction, disjunction, true, and false. For these logics we define both algebraic semantics, in the form of distributive modal algebras, and relational semantics, in the form of ordered Kripke structures. The main contributions of this paper lie in extending the notion of Sahlqvist axioms to our generalized setting and proving both a correspondence and a canonicity result for distributive modal logics axiomatized by Sahlqvist axioms. Our proof of the correspondence result relies on a reduction to the classical case, but our canonicity proof departs from the traditional style and uses the newly extended algebraic theory of canonical extensions.     

On squares of modal logics with additional connectives

The paper gives an overview of new results on two-dimensional modal logics of special type, “Segerberg squares.” They are defined as usual squares of modal logics with additional connectives corresponding to the diagonal symmetry and two projections onto the diagonal. In many cases these logics are finitely axiomatizable, complete and have the finite model property. Segerberg squares are interpreted in the classical predicate logic.     

Algebraization of the Three‐valued BCK‐logic

In this paper a definition of n‐valued system in the context of the algebraizable logics is proposed. We define and study the variety V₃, showing that it is definitionally equivalent to the equivalent quasivariety semantics for the “Three‐valued BCK‐logic”. As a consequence we find an axiomatic definition of the above system.     

Barwise's Information Frames and Modal Logics

The article studies Barwise's information frames and settles the problem of Barwise dealing in finding axiomatizations for the modal logics generated by information frames. We find axiomatic systems for: (i) the modal logic of all complete information frames; (ii) the logic of all sound and complete information frames; (iii) the logic of all hereditary and complete information frames; (iv) the logic of all complete, sound, and hereditary information frames; (v) the logic of all consistent and complete information frames. The notion of weak modal logics is also proposed, and it is shown that the weak modal logics generated by all information frames and by all hereditary information frames are K and K4, respectively. Toward a general theory, we prove that any Kripke complete modal logic is a modal logic of a certain class of information frames, and that every modal logic generated by any given class of complete, rarefied, and fully classified information frames is Kripke complete.     

Barwise's information frames and modal logics

 The paper studies Barwise's information frames and answers the John Barwise question: to find axiomatizations for the modal logics generated by information frames. We find axiomatic systems for (i) the modal logic of all complete information frames, (ii) the logic of all sound and complete information frames, (iii) the logic of all hereditary and complete information frames, (iv) the logic of all complete, sound and hereditary information frames, and (v) the logic of all consistent and complete information frames. The notion of weak modal logics is also proposed, and it is shown that the weak modal logics generated by all information frames and by all hereditary information frames are K and K4 respectively. To develop general theory, we prove that (i) any Kripke complete modal logic is the modal logic of a certain class of information frames and that (ii) the modal logic generated by any given class of complete, rarefied and fully classified information frames is Kripke complete. This paper is dedicated to the memory of talented mathematician John Barwise. Received: 7 May 2000 Published online: 10 October 2002 Key words or phrases: Knowledge presentation – Information – Information flow – Information frames – Modal logic-Kripke model     

On the Modal Logic of Jeffrey Conditionalization

We continue the investigations initiated in the recent papers (Brown et al. in The modal logic of Bayesian belief revision, 2017; Gyenis in Standard Bayes logic is not finitely axiomatizable, 2018) where Bayes logics have been introduced to study the general laws of Bayesian belief revision. In Bayesian belief revision a Bayesian agent revises (updates) his prior belief by conditionalizing the prior on some evidence using the Bayes rule. In this paper we take the more general Jeffrey formula as a conditioning device and study the corresponding modal logics that we call Jeffrey logics, focusing mainly on the countable case. The containment relations among these modal logics are determined and it is shown that the logic of Bayes and Jeffrey updating are very close. It is shown that the modal logic of belief revision determined by probabilities on a finite or countably infinite set of elementary propositions is not finitely axiomatizable. The significance of this result is that it clearly indicates that axiomatic approaches to belief revision might be severely limited.     

The structure of slices over minimal logic

In [1], we introduced a classification of extensions of Johansson’s minimal logic J by means of slices and proved the decidability of the classification. In this article, we find sufficiently simple necessary conditions for the maximality of logics in the slices formulated in terms of frames. This makes it possible to describe an efficient procedure for computing the slice number of any finitely axiomatizable logic over J. The maximal logics of the upper slices are written down explicitly.     

Bilattice logic of epistemic actions and knowledge

Baltag, Moss, and Solecki proposed an expansion of classical modal logic, called logic of epistemic actions and knowledge (EAK), in which one can reason about knowledge and change of knowledge. Kurz and Palmigiano showed how duality theory provides a flexible framework for modeling such epistemic changes, allowing one to develop dynamic epistemic logics on a weaker propositional basis than classical logic (for example an intuitionistic basis). In this paper we show how the techniques of Kurz and Palmigiano can be further extended to define and axiomatize a bilattice logic of epistemic actions and knowledge (BEAK). Our propositional basis is a modal expansion of the well-known four-valued logic of Belnap and Dunn, which is a system designed for handling inconsistent as well as potentially conflicting information. These features, we believe, make our framework particularly promising from a computer science perspective.     

Algorithmic correspondence and canonicity for non-distributive logics

We extend the theory of unified correspondence to a broad class of logics with algebraic semantics given by varieties of normal lattice expansions (LEs), also known as ‘lattices with operators’. Specifically, we introduce a syntactic definition of the class of Sahlqvist formulas and inequalities which applies uniformly to each LE-signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives. We also introduce the algorithm ALBA, parametric in each LE-setting, which effectively computes first-order correspondents of LE-inequalities, and is guaranteed to succeed on a wide class of inequalities (the so-called inductive inequalities) which significantly extend the Sahlqvist class. Further, we show that every inequality on which ALBA succeeds is canonical. Projecting these results on specific signatures yields state-of-the-art correspondence and canonicity theory for many well known modal expansions of classical and intuitionistic logic and for substructural logics, from classical poly-modal logics to (bi-)intuitionistic modal logics to the Lambek calculus and its extensions, the Lambek-Grishin calculus, orthologic, the logic of (not necessarily distributive) De Morgan lattices, and the multiplicative-additive fragment of linear logic.     

Note on grammatical translations of logical calculi

It is shown that there exists no grammatical translation into classical (propositional) logic of the modal logics, nor of intuitionistic logic and of the relatedness and dependence logics, as defined in Richard L. Epstein's bookThe Semantic foundations of logic. In the book the result is proved for translations without parameters.Classical propositional logicPC can be translated into other logics. Usually the grammatical structure of propositions is preserved, in the sense of the following definition.     

All finitely axiomatizable subframe logics containing the provability logic CSM_{0} are decidable

In this paper we investigate those extensions of the bimodal provability logic (alias or which are subframe logics, i.e. whose general frames are closed under a certain type of substructures. Most bimodal provability logics are in this class. The main result states that all finitely axiomatizable subframe logics containing are decidable. We note that, as a rule, interesting systems in this class do not have the finite model property and are not even complete with respect to Kripke semantics. Received July 15, 1997     

Kripke‐style semantics for many‐valued logics

This paper deals with Kripke‐style semantics for many‐valued logics. We introduce various types of Kripke semantics, and we connect them with algebraic semantics. As for modal logics, we relate the axioms of logics extending MTL to properties of the Kripke frames in which they are valid. We show that in the propositional case most logics are complete but not strongly complete with respect to the corresponding class of complete Kripke frames, whereas in the predicate case there are important many‐valued logics like BL, ? and Π, which are not even complete with respect to the class of all predicate Kripke frames in which they are valid. Thus although very natural, Kripke semantics seems to be slightly less powerful than algebraic semantics. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A proof-theoretical investigation of global intuitionistic (fuzzy) logic

We perform a proof-theoretical investigation of two modal predicate logics: global intuitionistic logic GI and global intuitionistic fuzzy logic GIF. These logics were introduced by Takeuti and Titani to formulate an intuitionistic set theory and an intuitionistic fuzzy set theory together with their metatheories. Here we define analytic Gentzen style calculi for GI and GIF. Among other things, these calculi allows one to prove Herbrands theorem for suitable fragments of GI and GIF.Work Supported by C. Bühler-Habilitations-Stipendium H191-N04, from the Austrian Science Fund (FWF).