In this paper, we study three representations of lattices by means of a set with a binary relation of compatibility in the tradition of Ploščica. The standard representations of complete ortholattices and complete perfect Heyting algebras drop out as special cases of the first representation, while the second covers arbitrary complete lattices, as well as complete lattices equipped with a negation we call a protocomplementation. The third topological representation is a variant of that of Craig, Haviar, and (...) Priestley. We then extend each of the three representations to lattices with a multiplicative unary modality; the representing structures, like so-called graph-based frames, add a second relation of accessibility interacting with compatibility. The three representations generalize possibility semantics for classical modal logics to non-classical modal logics, motivated by a recent application of modal orthologic to natural language semantics. (shrink)

In this paper we consider the class of truth-functional modal many-valued logics with the complete lattice of truth-values. The conjunction and disjunction logic operators correspond to the meet and join operators of the lattices, while the negation is independently introduced as a hierarchy of antitonic operators which invert bottom and top elements. The non-constructive logic implication will be defined for a subclass of modular lattices, while the constructive implication for distributive lattices (Heyting algebras) is based on relative (...) pseudo-complements as in intuitionistic logic. We show that the complete lattices are intrinsically modal, with banal identity modal operator. We define the autoreferential set-based representation for the class of modal algebras, and show that the autoreferential Kripke-style semantics for this class of modal algebras is based on the set of possible worlds equal to the complete lattice of algebraic truth-values. The philosophical assumption is based on the consideration that each possible world represents a level of credibility, so that only propositions with the right logic value (i.e., level of credibility) can be accepted by this world, then we connect it with paraconsistent properties and LFI logics. The bottom truth value in this complete lattice corresponds to the trivial world in which each formula is satisfied, that is, to the world with explosive inconsistency. The top truth value corresponds to the world with classical logics, while all intermediate possible worlds represent the different levels of paraconsistent logics. (shrink)

A structural theorem for Kleene algebras is proved, showing that an element of a Kleene algebra can be looked upon as an ordered pair of sets, and that negation with the Kleene property is describable by the set-theoretic complement. The propositional logic \ of Kleene algebras is shown to be sound and complete with respect to a 3-valued and a rough set semantics. It is also established that Kleene negation can be considered as a modal operator, due to (...) a perp semantics of \. Moreover, another representation of Kleene algebras is obtained in the class of complex algebras of compatibility frames. One concludes with the observation that \ can be imparted semantics from different perspectives. (shrink)

Epistemic modals have peculiar logical features that are challenging to account for in a broadly classical framework. For instance, while a sentence of the form ‘p, but it might be that not p’ appears to be a contradiction, 'might not p' does not entail 'not p', which would follow in classical logic. Likewise, the classical laws of distributivity and disjunctive syllogism fail for epistemic modals. Existing attempts to account for these facts generally either under- or over-correct. Some theories predict that (...) 'p and might not p', a so-called epistemic contradiction, is a contradiction only in an etiolated sense, under a notion of entailment that does not allow substitution of logical equivalents; these theories underpredict the infelicity of embedded epistemic contradictions. Other theories savage classical logic, eliminating not just rules that intuitively fail, like distributivity and disjunctive syllogism, but also rules like non-contradiction, excluded middle, De Morgan’s laws, and disjunction introduction, which intuitively remain valid for epistemic modals. In this paper, we aim for a middle ground, developing a semantics and logic for epistemic modals that makes epistemic contradictions genuine contradictions and that invalidates distributivity and disjunctive syllogism but that otherwise preserves classical laws that intuitively remain valid. We start with an algebraic semantics, based on ortholattices instead of Boolean algebras, and then propose a more concrete possibility semantics, based on partial possibilities related by compatibility. Both semantics yield the same consequence relation, which we axiomatize. Then we show how to extend our semantics to explain parallel phenomena involving probabilities and conditionals. The goal throughout is to retain what is desirable about classical logic while accounting for the non-classicality of epistemic vocabulary. (shrink)

The aim of this paper is to introduce a new approach to the modal operators of necessity and possibility. This approach is based on the existence of two negations in certain lattices that we call bi-Heyting algebras. Modal operators are obtained by iterating certain combinations of these negations and going to the limit. Examples of these operators are given by means of graphs.

Two algebraic structures, the contrapositionally complemented Heyting algebra (ccHa) and the contrapositionally |$\vee $| complemented Heyting algebra (c|$\vee $|cHa), are studied. The salient feature of these algebras is that there are two negations, one intuitionistic and another minimal in nature, along with a condition connecting the two operators. Properties of these algebras are discussed, examples are given and comparisons are made with relevant algebras. Intuitionistic Logic with Minimal Negation (ILM) corresponding to ccHas and its extension |${\textrm (...) {ILM}}$|-|${\vee }$| for c|$\vee $|cHas are then investigated. Besides its relations with intuitionistic and minimal logics, ILM is observed to be related to Peirce’s logic and Vakarelov’s logic MIN. With a focus on properties of the two negations, relational semantics for ILM and |${\textrm {ILM}}$|-|${\vee }$| are obtained with respect to four classes of frames, and inter-translations between the classes preserving truth and validity are provided. ILM and |${\textrm {ILM}}$|-|${\vee }$| are shown to have the finite model property with respect to these classes of frames and proved to be decidable. Extracting features of the two negations in the algebras, a further investigation is made, following logical studies of negations that define the operators independently of the binary operator of implication. Using Dunn’s logical framework for the purpose, two logics |$K_{im}$| and |$K_{im-{\vee }}$| are discussed, where the language does not include implication. The |$K_{im}$|-algebras are reducts of ccHas and are different from relevant algebraic structures having two negations. The negations in the |$K_{im}$|-algebras and |$K_{im-{\vee }}$|-algebras are shown to occupy distinct positions in an enhanced form of Dunn’s kite of negations. Relational semantics for |$K_{im}$| and |$K_{im-{\vee }}$| is provided by a class of frames that are based on Dunn’s compatibility frames. It is observed that this class coincides with one of the four classes giving the relational semantics for ILM and |${\textrm {ILM}}$|-|${\vee }$|⁠. (shrink)

The variety \(\mathbb{DHMSH}\) of dually hemimorphic semi-Heyting algebras was introduced in 2011 by the second author as an expansion of semi-Heyting algebras by a dual hemimorphism. In this paper, we focus on the variety \(\mathbb{DHMSH}\) from a logical point of view. The paper presents an extensive investigation of the logic corresponding to the variety of dually hemimorphic semi-Heyting algebras and of its axiomatic extensions, along with an equally extensive universal algebraic study of their corresponding algebraic semantics. (...) Firstly, we present a Hilbert-style axiomatization of a new logic called "Dually hemimorphic semi-Heyting logic" (\(\mathcal{DHMSH}\), for short), as an expansion of semi-intuitionistic logic \(\mathcal{SI}\) (also called \(\mathcal{SH}\)) introduced by the first author by adding a weak negation (to be interpreted as a dual hemimorphism). We then prove that it is implicative in the sense of Rasiowa and that it is complete with respect to the variety \(\mathbb{DHMSH}\). It is deduced that the logic \(\mathcal{DHMSH}\) is algebraizable in the sense of Blok and Pigozzi, with the variety \(\mathbb{DHMSH}\) as its equivalent algebraic semantics and that the lattice of axiomatic extensions of \(\mathcal{DHMSH}\) is dually isomorphic to the lattice of subvarieties of \(\mathbb{DHMSH}\). A new axiomatization for Moisil's logic is also obtained. Secondly, we characterize the axiomatic extensions of \(\mathcal{DHMSH}\) in which the "Deduction Theorem" holds. Thirdly, we present several new logics, extending the logic \(\mathcal{DHMSH}\), corresponding to several important subvarieties of the variety \(\mathbb{DHMSH}\). These include logics corresponding to the varieties generated by two-element, three-element and some four-element dually quasi-De Morgan semi-Heyting algebras, as well as a new axiomatization for the 3-valued Łukasiewicz logic. Surprisingly, many of these logics turn out to be connexive logics, only a few of which are presented in this paper. Fourthly, we present axiomatizations for two infinite sequences of logics namely, De Morgan Gödel logics and dually pseudocomplemented Gödel logics. Fifthly, axiomatizations are also provided for logics corresponding to many subvarieties of regular dually quasi-De Morgan Stone semi-Heyting algebras, of regular De Morgan semi-Heyting algebras of level 1, and of JI-distributive semi-Heyting algebras of level 1. We conclude the paper with some open problems. Most of the logics considered in this paper are discriminator logics in the sense that they correspond to discriminator varieties. Some of them, just like the classical logic, are even primal in the sense that their corresponding varieties are generated by primal algebras. (shrink)

Epistemic modals have peculiar logical features that are challenging to account for in a broadly classical framework. For instance, while a sentence of the form $$p\wedge \Diamond \lnot p$$ (‘p, but it might be that not p’) appears to be a contradiction, $$\Diamond \lnot p$$ does not entail $$\lnot p$$, which would follow in classical logic. Likewise, the classical laws of distributivity and disjunctive syllogism fail for epistemic modals. Existing attempts to account for these facts generally either under- or over-correct. (...) Some theories predict that $$ p\wedge \Diamond \lnot p$$, a so-called epistemic contradiction, is a contradiction only in an etiolated sense, under a notion of entailment that does not always allow us to replace $$p\wedge \Diamond \lnot p$$ with a contradiction; these theories underpredict the infelicity of embedded epistemic contradictions. Other theories savage classical logic, eliminating not just rules that intuitively fail, like distributivity and disjunctive syllogism, but also rules like non-contradiction, excluded middle, De Morgan’s laws, and disjunction introduction, which intuitively remain valid for epistemic modals. In this paper, we aim for a middle ground, developing a semantics and logic for epistemic modals that makes epistemic contradictions genuine contradictions and that invalidates distributivity and disjunctive syllogism but that otherwise preserves classical laws that intuitively remain valid. We start with an algebraic semantics, based on ortholattices instead of Boolean algebras, and then propose a possibility semantics, based on partial possibilities related by compatibility. Both semantics yield the same consequence relation, which we axiomatize. We then show how to lift an arbitrary possible worlds model for a non-modal language to a possibility model for a language with epistemic modals. The goal throughout is to retain what is desirable about classical logic while accounting for the non-classicality of epistemic vocabulary. (shrink)

We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deduction system for the logic that contains only the introduction and elimination rules for the logical constants. From this starting point, if one adds the rule that Fitch called Reiteration, one obtains a proof system for intuitionistic logic in the given (...) signature; if instead of adding Reiteration, one adds the rule of Reductio ad Absurdum, one obtains a proof system for orthologic; by adding both Reiteration and Reductio, one obtains a proof system for classical logic. Arguably neither Reiteration nor Reductio is as intimately related to the meaning of the connectives as the introduction and elimination rules are, so the base logic we identify serves as a more fundamental starting point and common ground between proponents of intuitionistic logic, orthologic, and classical logic. The algebraic semantics for the logic we motivate proof-theoretically is based on bounded lattices equipped with what has been called a weak pseudocomplementation. We show that such lattice expansions are representable using a set together with a reflexive binary relation satisfying a simple first-order condition, which yields an elegant relational semantics for the logic. This builds on our previous study of representations of lattices with negations, which we extend and specialize for several types of negation in addition to weak pseudocomplementation; in an appendix, we further extend this representation to lattices with implications. Finally, we discuss adding to our logic a conditional obeying only introduction and elimination rules, interpreted as a modality using a family of accessibility relations. (shrink)

We present a Kripke model for Girard's Linear Logic (without exponentials) in a conservative fashion where the logical functors beyond the basic lattice operations may be added one by one without recourse to such things as negation. You can either have some logical functors or not as you choose. Commutatively and associatively are isolated in such a way that the base Kripke model is a model for noncommutative, nonassociative Linear Logic. We also extend the logic by adding a coimplication operator, (...) similar to Curry's subtraction operator, which is resituated with Linear Logic's contensor product. And we can add contraction to get nondistributive Relevance Logic. The model rests heavily on Urquhart's representation of nondistributive lattices and also on Dunn's Gaggle Theory. Indeed, the paper may be viewed as an investigation into nondistributive Gaggle Theory restricted to binary operations. The valuations on the Kripke model are three valued: true, false, and indifferent. The lattice representation theorem of Urquhart has the nice feature of yielding Priestley's representation theorem for distributive lattices if the original lattice happens to be distributive. Hence the representation is consistent with Stone's representation of distributive and Boolean lattices, and our semantics is consistent with the Lemmon-Scott representation of modal algebras and the Routley-Meyer semantics for Relevance Logic. (shrink)

In so-called Kripke-type models, each sentence is assigned either to true or to false at each possible world. In this setting, every possible world has the two-valued Boolean algebra as the set of truth values. Instead, we take a collection of algebras each of which is attached to a world as the set of truth values at the world, and obtain an extended semantics based on the traditional Kripke-type semantics, which we call here the algebraic Kripke (...) semantics. We introduce algebraic Kripke sheaf semantics for super-intuitionistic and modal predicate logics, and discuss some basic properties. We can state the Gödel-McKinsey-Tarski translation theorem within this semantics. Further, we show new results on super-intuitionistic predicate logics. We prove that there exists a continuum of super-intuitionistic predicate logics each of which has both of the disjunction and existence properties and moreover the same propositional fragment as the intuitionistic logic. (shrink)

We prove completeness of the propositional modal logic S 4 for the measure algebra based on the Lebesgue-measurable subsets of the unit interval, [0, 1]. In recent talks, Dana Scott introduced a new measure-based semantics for the standard propositional modal language with Boolean connectives and necessity and possibility operators, and . Propositional modal formulae are assigned to Lebesgue-measurable subsets of the real interval [0, 1], modulo sets of measure zero. Equivalence classes of (...) Lebesgue-measurable subsets form a measure algebra, , and we add to this a non-trivial interior operator constructed from the frame of ‘open’ elements—elements in with an open representative. We prove completeness of the modal logic S 4 for the algebra . A corollary to the main result is that non-theorems of S 4 can be falsified at each point in a subset of the real interval [0, 1] of measure arbitrarily close to 1. A second corollary is that Intuitionistic propositional logic (IPC) is complete for the frame of open elements in. (shrink)

The notion of a context in formal concept analysis and that of an approximation space in rough set theory are unified in this study to define a Kripke context. For any context (G,M,I), a relation on the set G of objects and a relation on the set M of properties are included, giving a structure of the form ((G,R), (M,S), I). A Kripke context gives rise to complex algebras based on the collections of protoconcepts and semiconcepts of the underlying (...) context. On abstraction, double Boolean algebras (dBas) with operators and topological dBas are defined. Representation results for these algebras are established in terms of the complex algebras of an appropriate Kripke context. As a natural next step, logics corresponding to classes of these algebras are formulated. A sequent calculus is proposed for contextual dBas, modal extensions of which give logics for contextual dBas with operators and topological contextual dBas. The representation theorems for the algebras result in a protoconcept-based semantics for these logics. (shrink)

In this paper we define an augmentation mHC of the Heyting propositional calculus HC by a modal operator ?. This modalized Heyting calculus mHC is a weakening of the Proof-Intuitionistic Logic KM of Kuznetsov and Muravitsky. In Section 2 we present a short selection of attractive (algebraic, relational, topological and categorical) features of mHC. In Section 3 we establish some close connections between mHC and certain normal extension K4.Grz of the modal system K4. We define (...) a translation of mHC into K4.Grz and prove that this translation is exact, i. e. theorem-preserving and deducibility-invariant. We have established (however, in this note we do not present a proof of this) that the lattice of all extensions of mHC is isomorphic to the lattice of normal extensions of K4.Grz (a generalization of the Kuznetsov and Muravitsky theorem). (shrink)

A systematic approach to the algebraic and Kripke semantics for logics with restricted structural rules, notably for logics on an underlying non-distributive lattice, is developed. We provide a new topological representation theorem for general lattices, using the filter space X. Our representation involves a galois connection on subsets of X, hence a closure operator $\Gamma$, and the image of the representation map is characterized as the collection of $\Gamma$-stable, compact-open subsets of the filter space . The (...) original lattice ${\cal L}$ is thus imbedded in the complete lattice of stable sets. The representation is shown to be functorial and is extended to a Stone-type duality. ;In the presence of additional operators, the extension problem is addressed in terms of what we call adjoint completions of normal operators. An operator f on a lattice L is normal if f: $L\sp{} \times \cdots \times L\sp{} \to L\sp{}$ is a monotone map, where each $L\sp{}$, $i \in n$ + 1, is either L or $L\sp{op}$ and f sends finite joins of $L\sp{}$ to joins in $L\sp{}$. Every familiar operator, such as $\circ$ , + , $\gets, \to, \neg, \square$ O is normal. By a uniform argument we show that normal operators $f\sb{i}$ on L extend to operators $F\sb{i}$ on $\Gamma X$ that distribute over arbitrary joins or meets and that \sb{i\in I})$ is a universal such extension. ;We also raise and resolve the question of representability of operators on stable sets by relations. We give an extensive number of examples of representation of specific operators and provide explicit constructions of canonical Kripke frames, based on our extension arguments, for a number of logical systems, notably for Intuitionistic and Classical Linear Logics, or Non-commutative Linear Logic and of fragments thereof. (shrink)

This paper introduces the category of b-frames as a new tool in the study of complete lattices. B-frames can be seen as a generalization of posets, which play an important role in the representation theory of Heyting algebras, but also in the study of complete Boolean algebras in forcing. This paper combines ideas from the two traditions in order to generalize some techniques and results to the wider context of complete lattices. In particular, we lift a (...) class='Hi'>representation theorem of Allwein and MacCaull to a duality between complete lattices and b-frames, and we derive alternative characterizations of several classes of complete lattices from this duality. This framework is then used to obtain new results in the theory of complete Heyting algebras and the semantics of intuitionistic propositional logic. (shrink)

We prove frame determination results for the family of many-valued modal logics introduced by M. Fitting in the early '90s. Each modal language of this family is based on a Heyting algebra, which serves as the space of truth values, and is interpreted on an interesting version of possible-worlds semantics: the modal frames are directed graphs whose edges are labelled with an element of the underlying Heyting algebra. We introduce interesting generalized forms of (...) the classical axioms D, T, B, 4, and 5 and prove that they are canonical for certain algebraic frame properties, which generalize seriality, reflexivity, symmetry, transitivity and euclideanness. Our results are quite general as they hold for any modal language built on a complete Heyting algebra. (shrink)

We prove frame determination results for the family of many-valued modal logics introduced by M. Fitting in the early '90s. Each modal language of this family is based on a Heyting algebra, which serves as the space of truth values, and is interpreted on an interesting version of possible-worlds semantics: the modal frames are directed graphs whose edges are labelled with an element of the underlying Heyting algebra. We introduce interesting generalized forms of (...) the classical axioms D, T, B, 4, and 5 and prove that they are canonical for certain algebraic frame properties, which generalize seriality, reflexivity, symmetry, transitivity and euclideanness. Our results are quite general as they hold for any modal language built on a complete Heyting algebra. (shrink)

We give an equivalent formulation of topological algebras, interpreting S4, as boolean algebras equipped with intuitionistic negation. The intuitionistic substructure—Heyting algebra—of such an algebra can be then seen as an “epistemic subuniverse”, and modalities arise from the interaction between the intuitionistic and classical negations or, we might perhaps say, between the epistemic and the ontological aspects: they are not relations between arbitrary alternatives but between intuitionistic substructures and one common world governed by the classical (...) (propositional) logic. As an example of the generality of the obtained view, we apply it also to S5. We give a sound, complete and decidable sequent calculus, extending a classical system with the rules for handling the intuitionistic negation, in which one can prove all classical, intuitionistic and S4 valid sequents. (shrink)

This is Part 1 of a paper on fibred semantics and combination of logics. It aims to present a methodology for combining arbitrary logical systems L i , i ∈ I, to form a new system L I . The methodology `fibres' the semantics K i of L i into a semantics for L I , and `weaves' the proof theory (axiomatics) of L i into a proof system of L I . There are various ways of (...) doing this, we distinguish by different names such as `fibring', `dovetailing' etc, yielding different systems, denoted by L F I , L D I etc. Once the logics are `weaved', further `interaction' axioms can be geometrically motivated and added, and then systematically studied. The methodology is general and is applied to modal and intuitionistic logics as well as to general algebraic logics. We obtain general results on bulk, in the sense that we develop standard combining techniques and refinements which can be applied to any family of initial logics to obtain further combined logics. The main results of this paper is a construction for combining arbitrary, (possibly not normal) modal or intermediate logics, each complete for a class of (not necessarily frame) Kripke models. We show transfer of recursive axiomatisability, decidability and finite model property. Some results on combining logics (normal modal extensions of K) have recently been introduced by Kracht and Wolter, Goranko and Passy and by Fine and Schurz as well as a multitude of special combined systems existing in the literature of the past 20-30 years. We hope our methodology will help organise the field systematically. (shrink)

In this paper we continue the investigation of monadic Heyting algebras which we started in [2]. Here we present the representation theorem for monadic Heyting algebras and develop the duality theory for them. As a result we obtain an adequate topological semantics for intuitionistic modal logics over MIPC along with a Kripke-type semantics for them. It is also shown the importance and the effectiveness of the duality theory for further investigation of monadic (...) class='Hi'>Heyting algebras and logics over MIPC. (shrink)

Brouwer's views on the foundations of mathematics have inspired the study of intuitionistic logic, including the study of the intuitionistic propositional calculus and its extensions. The theory of these systems has become an independent branch of logic with connections to lattice theory, topology, modal logic and other areas. This paper aims to present a modern account of semantics for intuitionistic propositional systems. The guiding idea is that of a hierarchy of semantics, organized by increasing (...) generality: from the least general Kripke semantics on through Beth semantics, topological semantics, Dragalin semantics, and finally to the most general algebraic semantics. While the Kripke, topological, and algebraic semantics have been extensively studied, the Beth and Dragalin semantics have received less attention. We bring Beth and Dragalin semantics to the fore, relating them to the concept of a nucleus from pointfree topology, which provides a unifying perspective on the semantic hierarchy. (shrink)

The aim of the paper is to show that topoi are useful in the categorial analysis of the constructive logic with strong negation. In any topos ϵ we can distinguish an object Λ and its truth-arrows such that sets ϵ have a Nelson algebra structure. The object Λ is defined by the categorial counterpart of the algebraic FIDEL-VAKARELOV construction. Then it is possible to define the universal quantifier morphism which permits us to make the first order predicate calculus. The completeness (...) theorem is proved using the Kripke-type semantic defined by THOMASON. (shrink)

We present algebraic semantics for the classical logic of proofs based on Boolean algebras. We also extend the language of the logic of proofs in order to have a Boolean structure on proof terms and equality predicate on terms. Moreover, the completeness theorem and certain generalizations of Stone’s representation theorem are obtained for all proposed algebras.

On the base of the classical logic the connectives of necessity and possibility have the equivalent positions in this sense that each of them is definable by the other one. The consequence of this fact is the possibility to define of the both modalities using the connective of identity. Thus, the connective of propositional identity defining the congruence of the propositional language has become the base of the reconstruction of necessity operator in some modal systems. Already in (...) 1957 Greniewski [9] obtained system S5 on the base of the propositional calculus with identity. Next, Cresswell [3], [4] reconstructed S4 and S5 in a similar way. Systematic investigations of this problem were undertaken by Suszko within the broader frame of SCI programme [16], [17], [18]. The connections between modal connectives and the connective of identity settle some philosophical sense of both modalities. Something is necessary, if it is identical with a logical truth. If something is different from the negation of some logical truth, it is possible. It is however, the “ontological” characteristics typical for modalities defined on the base of the classical logic. The settling of similar connections between intuitionistic identity and intuitionistic modalities uncover the philosophical sense of the “epistemic” necessity and possibility. Unfortunately, the symmetry between the classical and intuitionistic case is not entire. The acceptance of both equalities: = ¬ ¬ and = ¬ ¬, in the intuitionistic logic yields the classical versions of both modalities . Thus, there is a problem with defining the connective of intuitionistic possibility by the connective of identity. In Sections 2 and 3 two “partial” solutions of the mentioned problem are presented. They are “partial” because the connective of possibility has undesirable properties. The second solution yields the strengthening of the necessity connective, too. The main aim of this paper is obtained in Section 5, where a definition of the intuitionistic possibility is given. This definition uses the new connective of nonidentity, presented in Section 4. The new approach bases on the idea that some connectives like implication, negation, identity, necessity are “Heyting's” ones. The case of possibility is different. Together with coimplication, weak negation, and nonidentity, possibility belongs to the so-called “Brouwerian” connectives. The connectives of the first kind have such property that in Kripke's style semantics their interpretations in each point of this semantics are related to the interpretations in next points. In the case of the “Brouwerian” connectives the interpretations in each point depend on the interpretations in previous points. In this sense, “Heyting's” connectives are interpreted from the point of view of the future, while the interpretations of the “Brouwerian” connectives are from the point of view of the past. The relations between nonidentity and possibility connectives allow to say that in temporal semantics something is possible in the moment a, if before a there was such moment b in which it was different from the contradiction. Thus, “something is possible” does not mean that it held once in the past. A broader philosophical remarks about the nature of intuitionistic possibility are contained in two Comments in the last Section. (shrink)

We present a semantic study of a family of modal intuitionistic linear systems, providing various logics with both an algebraic semantics and a relational semantics, to obtain completeness results. We call modality a unary operator on formulas which satisfies only one rale (regularity), and we consider any subsetW of a list of axioms which defines the exponential of course of linear logic. We define an algebraic semantics by interpreting the modality as a unary operation on (...) an IL-algebra. Then we introduce a relational semantics based on pretopologies with an additional binary relationr between information states. The interpretation of is defined in a suitable way, which differs from the traditional one in classical modal logic. We prove that such models provide a complete semantics for our minimal modal system, as well as, by requiring the suitable conditions onr (in the spirit of correspondence theory), for any of its extensions axiomatized by any subsetW as above. We also prove an embedding theorem for modal IL-algebras into complete ones and, after introducing the notion of general frame, we apply it to obtain a duality between general frames and modal IL-algebras. (shrink)

Intuitionistic propositional logic with Galois negations ( \(\mathsf {IGN}\) ) is introduced. Heyting algebras with Galois negations are obtained from Heyting algebras by adding the Galois pair \((\lnot,{\sim })\) and dual Galois pair \((\dot{\lnot },\dot{\sim })\) of negations. Discrete duality between GN-frames and algebras as well as the relational semantics for \(\mathsf {IGN}\) are developed. A Hilbert-style axiomatic system \(\mathsf {HN}\) is given for \(\mathsf {IGN}\), and Galois negation logics are defined as extensions of \(\mathsf {IGN}\). (...) We give the bi-tense logic \(\mathsf {S4N}_t\) which is obtained from the minimal tense extension of the modal logic \(\mathsf {S4}\) by adding tense operators. We give a new extended Gödel translation \(\tau \) and prove that \(\mathsf {IGN}\) is embedded into \(\mathsf {S4N}_t\) by \(\tau \). Moreover, every Kripke-complete Galois negation logic _L_ is embedded into its tense companion \(\tau (L)\). (shrink)

The overwhelming majority of the attempts in exploring the problems related to quantum logical structures and their interpretation have been based on an underlying set-theoretic syntactic language. We propose a transition in the involved syntactic language to tackle these problems from the set-theoretic to the category-theoretic mode, together with a study of the consequent semantic transition in the logical interpretation of quantum event structures. In the present work, this is realized by representing categorically the global structure of a quantum (...) algebra of events (or propositions) in terms of sheaves of local Boolean frames forming Boolean localization functors. The category of sheaves is a topos providing the possibility of applying the powerful logical classification methodology of topos theory with reference to the quantum world. In particular, we show that the topos-theoretic representation scheme of quantum event algebras by means of Boolean localization functors incorporates an object of truth values, which constitutes the appropriate tool for the definition of quantum truth-value assignments to propositions describing the behavior of quantum systems. Effectively, this scheme induces a revised realist account of truth in the quantum domain of discourse. We also include an Appendix, where we compare our topos-theoretic representation scheme of quantum event algebras with other categorial and topos-theoretic approaches. (shrink)

We often have to draw conclusions about states of machines in computer science and about states of knowledge and belief in artificial intelligence based on partial information. Nerode suggested using constructive logic as the language to express such deductions and also suggested designing appropriate intuitionistic Kripke frames to express the partial information. Following this program, Nerode and Wijesekera developed syntax, semantics and completeness for a system of intuitionistic dynamic logic for proving properties of concurrent programs. Like (...) all dynamics logics, this was a logic of many modalities, each expressing a program, but in intuitionistic rather than in classical logic. In that logic, both box and diamond are needed, but these two are not intuitionistically interdefinable and, worse, diamond does not distribute over ‘or’, except for sequential programs. This also happens in other contemplated computer science and AI applications, and leads outside the class of constructive logics investigated in the literature. The present paper fills this gap. We provide intuitionistic logics with independent box and diamond without assuming distribution of diamond over ‘or’. The completeness theorem is based on intuitionistic Kripke frames , but equipped with an additional, quite separate accessibility relation between worlds. In the interpretation of Nerode and Wijesekera , worlds under the partial order represent states of partial knowledge, the accessibility represents change in state of partial knowledge resulting from executing a specific program. But there are many other computer science interpretations. This formalism covers all computer science applications of which we are aware. We also give a cut elimination theorem and algebraic and topological formulations, since these present some new difficulties. Finally, these results were obtained prior to those in Nerode and Wijesekera. (shrink)

We introduce the bimodal logic , which is the extension of Bennett’s bimodal logic by Grzegorczyk’s axiom □→p)→p and show that the lattice of normal extensions of the intuitionistic modal logic WS5 is isomorphic to the lattice of normal extensions of , thus generalizing the Blok–Esakia theorem. We also introduce the intuitionistic modal logic WS5.C, which is the extension of WS5 by the axiom →, and the bimodal logic , which is the extension of Shehtman’s bimodal (...) logic by Grzegorczyk’s axiom, and show that the lattice of normal extensions of WS5.C is isomorphic to the lattice of normal extensions of. (shrink)

From the point of view of non-classical logics, Heyting's implication is the smallest implication for which the deduction theorem holds. This book studies properties of logical systems having some of the classical connectives and implication in the neighbourhood of Heyt ing's implication. I have not included anything on entailment, al though it belongs to this neighbourhood, mainly because of the appearance of the Anderson-Belnap book on entailment. In the later chapters of this book, I have included material that might (...) be of interest to the intuitionist mathematician. Originally, I intended to include more material in that spirit but I decided against it. There is no coherent body of material to include that builds naturally on the present book. There are some serious results on topological models, second order Beth and Kripke models, theories of types, etc., but it would require further research to be able to present a general theory, possibly using sheaves. That would have postponed pUblication for too long. I would like to dedicate this book to my colleagues, Professors G. Kreisel, M.O. Rabin and D. Scott. I have benefited greatly from Professor Kreisel's criticism and suggestions. Professor Rabin's fun damental results on decidability and undecidability provided the powerful tools used in obtaining the majority of the results reported in this book. Professor Scott's approach to non-classical logics and especially his analysis of the Scott consequence relation makes it possible to present Heyting's logic as a beautiful, integral part of non-classical logics. (shrink)

This paper treats a kind of a modal logic based on the intuitionistic propositional logic which arose from the provability predicate in the first order arithmetic. The semantics of this calculus is presented in both a relational and an algebraic way.Completeness theorems, existence of a characteristic model and of a characteristic frame, properties of FMP and FFP and decidability are proved.

Constructive logic with Nelson negation is an extension of the intuitionistic logic with a special type of negation expressing some features of constructive falsity and refutation by counterexample. In this paper we generalize this logic weakening maximally the underlying intuitionistic negation. The resulting system, called subminimal logic with Nelson negation, is studied by means of a kind of algebras called generalized N-lattices. We show that generalized N-lattices admit representation formalizing the intuitive idea of refutation by means of (...) counterexamples giving in this way a counterexample semantics of the logic in question and some of its natural extensions. Among the extensions which are near to the intuitionistic logic are the minimal logic with Nelson negation which is an extension of the Johansson's minimal logic with Nelson negation and its in a sense dual version — the co-minimal logic with Nelson negation. Among the extensions near to the classical logic are the well known 3-valued logic of Lukasiewicz, two 12-valued logics and one 48-valued logic. Standard questions for all these logics — decidability, Kripke-style semantics, complete axiomatizability, conservativeness are studied. At the end of the paper extensions based on a new connective of self-dual conjunction and an analog of the Lukasiewicz middle value ½ have also been considered. (shrink)

The volume under review contains work dedicated to the memory of Leo Esakia, who died in 2010, after having worked for over 40 years towards developing duality theory for modal and intuitionistic logics. The collection comprises ten technical contributions that follow the first chapter, in which the reader can find information on Esakia’s studies and career, as well as a complete list of his research publications. In the sequel, we will refer briefly to each of these ten chapters, (...) following the order in the list of contents.B. Jónsson and A. Tarski, in two papers they published in the early 1950s in the American Journal of Mathematics, initiated the study of duality for Boolean algebras with additional operations, via the theory of canonical extensions. Esakia was among the first researchers who studied duality for lattices with additional operations [Topological Kripke models. Soviet Math.Dokl. 15 , 147–151], in particular for Heyting algebras and S4 modal algebras. M. Gehrke, a .. (shrink)

We present three examples of topological semantics for intuitionistic modal logic with one modal operator □. We show that it is possible to treat neighborhood models, introduced earlier, as topological or multi-topological. From the neighborhood point of view, our method is based on differences between properties of minimal and maximal neighborhoods. Also we propose transformation of multitopological spaces into the neighborhood structures.

Hyperboolean algebras are Boolean algebras with operators, constructed as algebras of complexes (or, power structures) of Boolean algebras. They provide an algebraic semantics for a modal logic (called here a {\em hyperboolean modal logic}) with a Kripke semantics accordingly based on frames in which the worlds are elements of Boolean algebras and the relations correspond to the Boolean operations. We introduce the hyperboolean modal logic, give a complete axiomatization of it, (...) and show that it lacks the finite model property. The method of axiomatization hinges upon the fact that a "difference" operator is definable in hyperboolean algebras, and makes use of additional non-Hilbert-style rules. Finally, we discuss a number of open questions and directions for further research. (shrink)

A method of defining semantics of logics based on not necessarily distributive lattices is presented. The key elements of the method are representation theorems for lattices and duality between classes of lattices and classes of some relational systems . We suggest a type of duality referred to as a duality via truth which leads to Kripke-style semantics and three-valued semantics in the style of Allwein-Dunn. We develop two new representation theorems for lattices which, together (...) with the existing theorems by Urquhart and Bimbo-Dunn, constitute a complete, in a sense, representation theory for lattices. As observed by Dunn and Hardegree, variations of Urquhart's duality arise by varying his disjointness assumption on the canonical frame. Four possible assumptions – disjoint, exhaustive, non-disjoint and non-exhaustive – are discussed in the paper. Each of the four corresponding representation theorems is expanded to a duality via truth. Based on these dualities we suggest four corresponding types of semantics for lattice-based logics. We also discuss a new topological representation of lattices. (shrink)

In this paper we will study a formal system of intuitionistic modal predicate logic. The main result is its semantic completeness theorem with respect to algebraic structures. At the end of the paper we will also present a brief consideration of its syntactic relationships with some similar systems.

It is a classic result in lattice theory that a poset is a complete lattice iff it can be realized as fixpoints of a closure operator on a powerset. Dragalin [9,10] observed that a poset is a locale (complete Heyting algebra) iff it can be realized as fixpoints of a nucleus on the locale of upsets of a poset. He also showed how to generate a nucleus on upsets by adding a structure of “paths” to a poset, forming what (...) we call a Dragalin frame. This allowed Dragalin to introduce a semantics for intuitionistic logic that generalizes Beth and Kripke semantics. He proved that every spatial locale (locale of open sets of a topological space) can be realized as fixpoints of the nucleus generated by a Dragalin frame. In this paper, we strengthen Dragalin’s result and prove that every locale—not only spatial locales—can be realized as fixpoints of the nucleus generated by a Dragalin frame. In fact, we prove the stronger result that for every nucleus on the upsets of a poset, there is a Dragalin frame based on that poset that generates the given nucleus. We then compare Dragalin’s approach to generating nuclei with the relational approach of Fairtlough and Mendler [11], based on what we call FM-frames. Surprisingly, every Dragalin frame can be turned into an equivalent FM-frame, albeit on a different poset. Thus, every locale can be realized as fixpoints of the nucleus generated by an FM-frame. Finally, we consider the relational approach of Goldblatt [13] and characterize the locales that can be realized using Goldblatt frames. (shrink)

ABSTRACTCorrespondence and Shalqvist theories for Modal Logics rely on the simple observation that a relational structure is at the same time the basis for a model of modal logic and for a model of first-order logic with a binary predicate for the accessibility relation. If the underlying set of the frame is split into two components,, and, then frames are at the same time the basis for models of non-distributive lattice logic and of two-sorted, residuated modal logic. (...) This suggests that a reduction of the first to the latter may be possible, encoding Positive Lattice Logic as a fragment of Two-Sorted, Residuated Modal Logic. The reduction is analogous to the well-known Gödel-McKinsey-Tarski translation of Intuitionistic Logic into the S4 system of normal modal logic. In this article, we carry out this reduction in detail and we derive some properties of PLL from corresponding properties of First-Order Logic. The reduction we present is extendible to the case of lattices with operators, making use of recent results by this author on the relational representation of normal lattice expansions. (shrink)

In "A Problem in Possible-World Semantics," David Kaplan presented a consistent and intelligible modal principle that cannot be validated by any possible world frame (in the terminology of modal logic, any neighborhood frame). However, Kaplan's problem is tempered by the fact that his principle is stated in a language with propositional quantification, so possible world semantics for the basic modal language without propositional quantifiers is not directly affected, and the fact that on careful inspection his (...) principle does not target the world part of possible world semantics—the atomicity of the algebra of propositions—but rather the idea of propositional quantification over a complete Boolean algebra of propositions. By contrast, in this paper we present a simple and intelligible modal principle, without propositional quantifiers, that cannot be validated by any possible world frame precisely because of their assumption of atomicity (i.e., the principle also cannot be validated by any atomic Boolean algebra expansion). It follows from a theorem of David Lewis that our logic is as simple as possible in terms of modal nesting depth (two). We prove the consistency of the logic using a generalization of possible world semantics known as possibility semantics. We also prove the completeness of the logic (and two other relevant logics) with respect to possibility semantics. Finally, we observe that the logic we identify naturally arises in the study of Peano Arithmetic. (shrink)

We generalize the double negation construction of Boolean algebras in Heyting algebras to a double negation construction of the same in Visser algebras. This result allows us to generalize Glivenko’s theorem from intuitionistic propositional logic and Heyting algebras to Visser’s basic propositional logic and Visser algebras.

In "An Alternative Semantics for Quantified Relevant Logic" (JSL 71 (2006)) we developed a semantics for quantified relevant logic that uses general frames. In this paper, we adapt that model theory to treat quantified modal logics, giving a complete semantics to the quantified extensions, both with and without the Barcan formula, of every proposi- tional modal logic S. If S is canonical our models are based on propositional frames that validate S. We employ frames (...) in which not every set of worlds is an admissible proposition, and an alternative interpretation of the uni- versal quantifier using greatest lower bounds in the lattice of admissible propositions. Our models have a fixed domain of individuals, even in the absence of the Barcan formula. For systems with the Barcan formula it is possible to preserve the usual Tarskian reading of the quantifier, at the expensive of sometimes losing va- lidity of S in the underlying propositional frames. We apply our results to a number of logics, including S4.2, S4M and KW, whose quantified extensions are incomplete for the standard semantics. (shrink)

I propose a comprehensive account of negation as a modal operator, vindicating a moderate logical pluralism. Negation is taken as a quantifier on worlds, restricted by an accessibility relation encoding the basic concept of compatibility. This latter captures the core meaning of the operator. While some candidate negations are then ruled out as violating plausible constraints on compatibility, different specifications of the notion of world support different logical conducts for negations. The approach unifies in a philosophically motivated picture the (...) following results: nothing can be called a negation properly if it does not satisfy Contraposition and Double Negation Introduction; the pair consisting of two split or Galois negations encodes a distinction without a difference; some paraconsistent negations also fail to count as real negations, but others may; intuitionistic negation qualifies as real negation, and classical Boolean negation does as well, to the extent that constructivist and paraconsistent doubts on it do not turn on the basic concept of compatibility but rather on the interpretation of worlds. (shrink)

In this paper we study the variety \(\textsf{WL}\) of bounded distributive lattices endowed with an implication, called weak Lewis distributive lattices. This variety corresponds to the algebraic semantics of the \(\{\vee,\wedge,\Rightarrow,\bot,\top \}\) -fragment of the arithmetical base preservativity logic \(\mathsf {iP^{-}}\). The variety \(\textsf{WL}\) properly contains the variety of bounded distributive lattices with strict implication, also known as weak Heyting algebras. We introduce the notion of WL-frame and we prove a representation theorem for WL-lattices by means of (...) WL-frames. We extended this representation to a topological duality by means of Priestley spaces endowed with a special neighbourhood relation between points and closed upsets of the space. These results are applied in order to give a representation and a topological duality for the variety of weak Heyting–Lewis algebras, i.e., for the algebraic semantics of the arithmetical base preservativity logic \(\textsf{iP}^{-}\). (shrink)

In a classical paper [15] V. Glivenko showed that a proposition is classically demonstrable if and only if its double negation is intuitionistically demonstrable. This result has an algebraic formulation: the double negation is a homomorphism from each Heyting algebra onto the Boolean algebra of its regular elements. Versions of both the logical and algebraic formulations of Glivenko’s theorem, adapted to other systems of logics and to algebras not necessarily related to logic can be found in the literature (...) (see [2, 9, 8, 14] and [13, 7, 14]). The aim of this paper is to offer a general frame for studying both logical and algebraic generalizations of Glivenko’s theorem. We give abstract formulations for quasivarieties of algebras and for equivalential and algebraizable deductive systems and both formulations are compared when the quasivariety and the deductive system are related. We also analyse Glivenko’s theorem for compatible expansions of both cases. (shrink)

Peirce introduced Existential Graphs in late 1896, and they were systematically investigated in his 1903 Lowell Lectures. Alpha graphs for classical propositional logic constitute the first part of EGs. The second and the third parts are the beta graphs for first-order logic and the gamma graphs for modal and higher-order logics, among others. As a logical syntax, EGs are two-dimensional graphs, or diagrams, in contrast to the linear algebraic notations. Peirce's theory of EGs is not only a theory of (...) logical syntax but also a proof theory for many logics. A set of transformation rules of graphs defines a proof system for a graphical logic. In this... (shrink)

Inquisitive logic is a research program seeking to expand the purview of logic beyond declarative sentences to include the logic of questions. To this end, inquisitive propositional logic extends classical propositional logic for declarative sentences with principles governing a new binary connective of inquisitive disjunction, which allows the formation of questions. Recently inquisitive logicians have considered what happens if the logic of declarative sentences is assumed to be intuitionistic rather than classical. In short, what should inquisitive logic be on (...) an intuitionistic base? In this paper, we provide an answer to this question from the perspective of nuclear semantics, an approach to classical and intuitionistic semantics pursued in our previous work. In particular, we show how Beth semantics for intuitionistic logic naturally extends to a semantics for inquisitive intuitionistic logic. In addition, we show how an explicit view of inquisitive intuitionistic logic comes via a translation into propositional lax logic, whose completeness we prove with respect to Beth semantics. (shrink)

ABSTRACT The two main directions pursued in the present paper are the following. The first direction was started by Pigozzi in 1969. In [Mak 91] and [Mak 79] Maksimova proved that a normal modal logic has the Craig interpolation property iff the corresponding class of algebras has the superamalgamation property. In this paper we extend Maksimova's theorem to normal multi-modal logics with arbitrarily many, not necessarily unary modalities, and to not necessarily normal multi-modal logics with modalities of (...) ranks smaller than 2. To extend the characterization beyond multi-modal logics, we look at arbitrary algebraizable logics. We will introduce an algebraic property equivalent with the Craig interpolation property in algebraizable logics, and prove that the superamalgamation property implies the Craig interpolation property. The problem of extending the characterization result to non-normal non-unary modal logics also will be discussed. In the second direction pursued herein: for non-normal modal logic with one unary modality Lemmon [Lem 66] gave a possible worlds semantics. Here we give a more general possible worlds semantics for not necessarily normal multi-modal logics with arbitrarily many not necessarily unary modalities. Strongly related to the above is the theorem, proved, e.g., in Jóns son-Tarski [JT 52] and Henkin-Monk-Tarski [HMT 71], that every normal Boolean algebra with operators can be represented as a subalgebra of the complex algebra of some relational structure. We extend this result to not necessarily normal BAO's as follows. We define partial relational structures and show that every not necessarily normal BAO is embeddable into the complex algebra of a partial relational structure. This gives a possible worlds semantics for not necessarily normal multi-modal logics. (shrink)

Logics designed to deal with vague statements typically allow algebraic semantics such that propositions are interpreted by elements of residuated lattices. The structure of these algebras is in general still unknown, and in the cases that a detailed description is available, to understand its significance for logics can be difficult. So the question seems interesting under which circumstances residuated lattices arise from simpler algebras in some natural way. A possible construction is described in this paper.Namely, we consider pairs consisting (...) of a Brouwerian algebra and an equivalence relation. The latter is assumed to be in a certain sense compatible with the partial order, with the formation of differences, and with the formation of suprema of pseudoorthogonal elements; we then call it an s-equivalence relation. We consider operations which, under a suitable additional assumption, naturally arise on the quotient set. The result is that the quotient set bears the structure of a residuated lattice. Further postulates lead to dual BL-algebras. In the case that we begin with Boolean algebras instead, we arrive at dual MV-algebras. (shrink)