LetL be any modal or tense logic with the finite model property. For eachm, definer L (m) to be the smallest numberr such that for any formulaA withm modal operators,A is provable inL if and only ifA is valid in everyL-model with at mostr worlds. Thus, the functionr L determines the size of refutation Kripke models forL. In this paper, we will give an estimation ofr L (m) for some linear modal and tense logicsL.

A many-valued modal logic, called linear abelian modal logic \(\rm {\mathbf{LK(A)}}\) is introduced as an extension of the abelian modal logic \(\rm \mathbf{K(A)}\). Abelian modal logic \(\rm \mathbf{K(A)}\) is the minimal modal extension of the logic of lattice-ordered abelian groups. The logic \(\rm \mathbf{LK(A)}\) is axiomatized by extending \(\rm \mathbf{K(A)}\) with the modal axiom schemas \(\Box(\varphi\vee\psi)\rightarrow(\Box\varphi\vee\Box\psi)\) and \((\Box\varphi\wedge\Box\psi)\rightarrow\Box(\varphi\wedge\psi)\). Completeness theorem with respect to algebraic semantics and a hypersequent calculus admitting cut-elimination are established. Finally, the correspondence between hypersequent calculi and (...) axiomatization is investigated. (shrink)

Temporal justification logic is a new family of temporal logics of knowledge in which the knowledge of agents is modelled using a justification logic. In this paper, we present various temporal justification logics involving both past and future time modalities. We combine Artemov’s logic of proofs with linear temporal logic with past, and we also investigate several principles describing the interaction of justification and time. We present two kinds of semantics for our temporal justification logics, one based on (...) interpreted systems and Fitting models and the other based on Mkrtychev models, and further, we establish soundness and completeness. We show that the internalization property holds in some of the temporal justification logics. We further investigate the two well-known epistemic-temporal notions of no forgetting and no learning in the framework of justification logics. Finally, we present temporal justification logics that avoid the logical omniscience problem. (shrink)

We present a sequent calculus for the modal logic S4, and building on some relevant features of this system we show how S4 can easily be translated into full propositional linear logic, extending the Grishin-Ono translation of classical logic into linear logic. The translation introduces linear modalities only in correspondence with S4 modalities. We discuss the complexity of the decision problem for several classes of linear formulas naturally arising from the proposed translations.

This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of linear logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic linear logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of (...) Kripke resource models extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatisation and a Gentzen-style sequent calculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequent calculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the l.. (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)

We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment (...) of GLP Λ. (shrink)

The paper aims at providing the multi-modal propositional logic LTK with a sound and complete axiomatisation. This logic combines temporal and epistemic operators and focuses on m odeling the behaviour of a set of agents operating in a system on the background of a temporal framework. Time is represented as linear and discrete, whereas knowledge is modeled as an S5-like modality. A further modal operator intended to represent environment knowledge is added to the system in order to achieve the (...) expressive power sufficient to describe the piece of information available to the agents at each moment in the flow of time. (shrink)

This paper proposes a semantic description of the linear step-like temporal multi-agent logic with the universal modality \(\mathcal{LTK}.sl_U\) based on the idea of non-reflexive non-transitive nature of time. We proved a finite model property and projective unification for this logic.

We introduce modal propositional substructural logics with strong negation, and prove the completeness theorems (with respect to Kripke models) for these logics.

The paper studies the logic TL(NBox+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities Diamond+ (possible in future) and Diamond- (possible in past) and special temporal operations, – Box+w (weakly necessary in future) and Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(NBox+-wC), so we prove that TL(NBox+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in (...) special reduced normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(NBox+-wC) and show how to reduce the problem for admissibility to the decidability of TL(NBox+-wC) itself using definable universal modalities. (shrink)

The present paper introduces and studies the variety [MATHEMATICAL SCRIPT CAPITAL W]ℋn of n-linear weakly Heyting algebras. It corresponds to the algebraic semantic of the strict implication fragment of the normal modal logic K with a generalization of the axiom that defines the linear intuitionistic logic or Dummett logic. Special attention is given to the variety [MATHEMATICAL SCRIPT CAPITAL W]ℋ2 that generalizes the linear Heyting algebras studied in [10] and [12], and the linear Basic algebras introduced (...) in [2]. (shrink)

This paper investigates logical aspects of combining linear orders as semantics for modal and temporal logics, with modalities for possible paths, resulting in a variety of branching time logics over classes of trees. Here we adopt a unified approach to the Priorean, Peircean and Ockhamist semantics for branching time logics, by considering them all as fragments of the latter, obtained as combinations, in various degrees, of languages and semantics for linear time with a modality for possible paths. (...) We then consider a hierarchy of natural classes of trees and bundled trees arising from a given class of linear orders and show that in general they provide different semantics. We also discuss transfer of definability from linear orders to trees and introduce a uniform translation from Priorean to Peircean formulae which transfers definability of properties of linear orders to definability of properties of all paths in trees. (shrink)

Variants of classical linear logics are presented based on the modal version of new structural rule !?mingle instead of the known rules !weakening and ?weakening. The cut-elimination theorems, the completeness theorems and a characteristic property named the mix separation principle are proved for these logics.

In an unpublished note Reddy introduced an extended intuitionistic linear calculus, called LLMS (for Linear Logic Model of State), to model state manipulation via the notions of sequential composition and ‘regenerative values’. His calculus introduces the connective ‘before’ ▹ and an associated modality †, for the storage of objects sequentially reusable. Earlier and independently de Paiva introduced a (collection of) dialectica categorical models for (classical and intuitionistic) Linear Logic, the categories Dial2Set. These categories contain, apart from the (...) structure needed to model linear logic, an extra tensor product functor and an extra comonad structure corresponding to a modality related to the extra tensor product. It is surprising that these works arising from completely different motivations can be related in a meaningful way. In this article, following joint work with Corrêa and Haeusler, we first adapt Reddy's system LLMS providing a commutative version of the connective ‘before’ and its associated modality and then construct a dialectica category on Sets , which we show is a sound model for the modified version of Reddy's the system LLMSc. Moreover, following the work of Tucker, we provide another variant of the Dialectica categories with a non-commutative tensor and its associated modality, which models soundlyLLMS itself. We conclude with some speculation on future applications. (shrink)

The goal of this paper is to show how modal logic may be conceived as recording the derived rules of a logical system in the system itself. This conception of modal logic was propounded by Dana Scott in the early seventies. Here, similar ideas are pursued in a context less classical than Scott's.First a family of propositional logical systems is considered, which is obtained by gradually adding structural rules to a variant of the nonassociative Lambek calculus. In this family one (...) finds systems that correspond to the associative Lambek calculus, linear logic, relevant logics, BCK logic and intuitionistic logic. Above these basic systems, sequent systems parallel to the basic systems are constructed, which formalize various notions of derived rules for the basic systems. The deduction theorem is provable for the basic systems if, and only if, they are at least as strong as systems corresponding to linear logic, or BCK logic, depending on the language, and their deductive metalogic is not stronger than they are. (shrink)

In the last two decades modal logic has undergone an explosive growth, to thepointthatacompletebibliographyofthisbranchoflogic,supposingthat someone were capable to compile it, would?ll itself a ponderous volume. What is impressive in the growth of modal logic has not been so much the quick accumulation of results but the richness of its thematic dev- opments. In the 1960s, when Kripke semantics gave new credibility to the logic of modalities? which was already known and appreciated in the Ancient and Medieval times? no one (...) could have foreseen that in a short time modal logic would become a lively source of ideas and methods for analytical philosophers,historians of philosophy,linguists, epistemologists and computer scientists. The aim which oriented the composition of this book was not to write a new manual of modal logic buttoo?ertoeveryreader,evenwithnospeci?cbackground in logic, a conceptually linear path in the labyrinth of the current panorama of modal logic. The notion which in our opinion looked suitable to work as a compass in this enterprise was the notion of multimodality, or, more speci?cally, the basic idea of grounding systems on languages admitting more than one primitive modal operator. (shrink)

The question at issue is to develop a computational interpretation of Linear Logic [8] and to establish exactly its expressive power. We follow the bottom-up approach. This involves starting with the simplest of the systems we are interested in, and then expanding them step-by-step. We begin with the !-Horn fragment of Linear Logic, which uses only positive literals, the linear implication ⊸, the tensor product ⊗, and the modal storage operator !. We give a complete computational interpretation (...) for the !-Horn fragment of Linear Logic and for some natural generalizations of it formed by introducing additive connectives. Here we use the well-known ‘ or ’-like connective ⊕, and, for the sake of the computational duality, we introduce a new ‘ and ’-like connective @ For !-Horn sequents, we prove that their derivability problem is directly equivalent to the reachability problem for Petri nets, which is known to be decidable [19]. For the -Horn fragment of Linear Logic, which uses only positive literals, the linear implication ⊸, the tensor product ⊗, the modal storage operator!, and the additive ‘disjunction’ ⊕, we prove that standard Minsky machines [21] can be directly encoded in this -Horn fragment. Standard Minsky machines can be directly encoded in the corresponding ‘dual’ -Horn fragment of Linear Logic, as well. As a corollary, both these fragments of Linear Logic are proved to be undecidable. (shrink)

Linear logic, introduced by Girard, is a refinement of classical logic with a natural, intrinsic accounting of resources. This accounting is made possible by removing the ‘structural’ rules of contraction and weakening, adding a modal operator and adding finer versions of the propositional connectives. Linear logic has fundamental logical interest and applications to computer science, particularly to Petri nets, concurrency, storage allocation, garbage collection and the control structure of logic programs. In addition, there is a direct correspondence between (...) polynomial-time computation and proof normalization in a bounded form of linear logic. In this paper we show that unlike most other propositional logics, full propositional linear logic is undecidable. Further, we prove that without the modal storage operator, which indicates unboundedness of resources, the decision problem becomes PSPACE-complete. We also establish membership in NP for the multiplicative fragment, NP-completeness for the multiplicative fragment extended with unrestricted weakening, and undecidability for fragments of noncommutative propositional linear logic. (shrink)

In this paper we continue the study of Girard's Linear Logic and introduce a new Linear Logic with modalities. Our logic describes not only the consumption, but also the presence of resources. We introduce a new semantics and a new calculus for this logic. In contrast to the results of Lincoln [7] and Kanovich [4] about the NP-completeness of the problem of the construction of a proof for a given sequent in the multiplicative fragment of Girard's (...) class='Hi'>Linear Logic, we present here a non-exponential algorithm to construct a proof for a given sequent and a given point of a given model in our Linear Logic. (shrink)

After the seminal work of Kraus, Lehmann and Magidor (formally known as the KLM approach) on conditionals and preferential models, many aspects of defeasibility in more complex formalisms have been studied in recent years. Examples of these aspects are the notion of typicality in description logic and defeasible necessity in modal logic. We discuss a new aspect of defeasibility that can be expressed in the case of temporal logic, which is the normality in an execution. In this contribution, we take (...) Linear Temporal Logic (LTL) as case study for this defeasible aspect. LTL has found extensive applications in Computer Science and Artificial Intelligence, notably as a formal framework for representing and verifying computer systems that vary over time. However, some systems may presents exceptions at some innocuous time points where they can be tolerated, or conversely, exceptions at other crucial time points where they need to be addressed. In order to ensure the reliability of such systems, we study a preferential extension of LTL, called defeasible linear temporal logic (LTL ~ ). In the first part of this paper, we show how semantics of KLM's preferential models can be integrated with LTL. We also discuss the addition of non-monotonic temporal operators as a way to formalise defeasible properties of these systems. The second part of this paper is a study of the satisfiability problem of LTL ~ sentences. Based on Sistla and Clarke's work on the complexity of the classical LTL language, we show the bounded-model property of two fragments of LTL ~ language. Moreover, we provide a procedure to check the satisfiability of sentences in both of these fragments. (shrink)

We present the propositional logic LEC for the two epistemic modalities of current and stable knowledge used by an agent who system-atically enriches his language. A change in the linguistic resources of an agent as a result of certain cognitive processes is something that commonly happens. Our system is based on the logic LC intended to formalize the idea that the occurrence of changes induces the passage of time. Here, the primitive operator C read as: it changes that, defines (...) the temporal succession of states of the world. The notion of current knowledge concerns variable components of the world and it may change over time. We represent it by the primitive operator k read as: the agent currently knows that, and assume that it has S5 properties. The second type of knowledge, symbolized by the primitive operator K read as: the agent stably knows that, relates to constant components of the world and it does not change. As a result of the axiomatic entanglement of C, K and k we show that stable knowledge satisfies axioms of S4.3. K and k modalities are not mutually definable, stable knowledge implies the current one and if the latter never changes, then it comes to be stable. The combination of K and k with the idea of an expanding language allows questioning of the so-called perfect recall principle. It cannot be maintained for both types of knowledge just because of changes in the vocabulary of the agent and possibly the growing spectrum of possible states of the world. We interpret LEC in the semantics of histories of epistemic changes and show that it is complete. Finally, we compare our logic with selected epistemic logics based on the concept of linear discrete time. (shrink)

We investigate the dynamics of sensory integration for perceiving musical performance, a complex natural behavior. Thirty musically trained participants saw, heard, or both saw and heard, performances by two clarinetists. All participants used a sliding potentiometer to make continuous judgments of tension (a measure correlated with emotional response) and continuous judgments of phrasing (a measure correlated with perceived musical structure) as performances were presented. The data analysis sought to reveal relations between the sensory modalities (vision and audition) and to (...) quantify the effect of seeing the performances on participants' overall subjective experience of the music. In addition to traditional statistics, functional data analysis techniques were employed to analyze time-varying aspects of the data. The auditory and visual channels were found to convey similar experiences of phrasing but different experiences of tension through much of the performances. We found that visual information served both to augment and to reduce the experience of tension at different points in the musical piece (as revealed by functional linear modeling and functional significance testing). In addition, the musicians' movements served to extend the sense of phrasing, to cue the beginning of new phrases, to indicate musical interpretation, and to anticipate changes in emotional content. Evidence for an interaction effect suggests that there may exist an emergent quality when musical performances are both seen and heard. The investigation augments knowledge of human communicative processes spanning language and music, and involving multiple modalities of emotion and information transfer. (shrink)

We investigate the semantics of the logical systems obtained by introducing the modalities and into the family of substructural implication logics (including relevant, linear and intuitionistic implication). Then, in the spirit of the LDS (Labelled Deductive Systems) methodology, we "import" this semantics into the classical proof system KE. This leads to the formulation of a uniform labelled refutation system for the new logics which is a natural extension of a system for substructural implication developed by the first two (...) authors in a previous paper. (shrink)

Substructural logics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructural logics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S4-type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings into analogues of S4 are obtained (...) with the help of cut elimination for sequent formulations of our substructural logics and their modal extensions. These results are proved for systems with equality too. (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)

We introduce Kripke semantics for modal substructural logics, and provethe completeness theorems with respect to the semantics. Thecompleteness theorems are proved using an extended Ishihara's method ofcanonical model construction (Ishihara, 2000). The framework presentedcan deal with a broad range of modal substructural logics, including afragment of modal intuitionistic linear logic, and modal versions ofCorsi's logics, Visser's logic, Méndez's logics and relevant logics.

We introduce an extended intuitionistic linear logic with strong negation and modality. The logic presented is a modal extension of Wansing's extended linear logic with strong negation. First, we propose three types of cut-free sequent calculi for this new logic. The first one is named a subformula calculus, which yields the subformula property. The second one is termed a dual calculus, which has positive and negative sequents. The third one is called a triple-context calculus, which is regarded as (...) a natural extension or generalization of Hodas and Miller's dual-context calculus appearing in a linear logic programming language. Second, we present a concurrent process calculus based on the logic. This calculus is an extension of Okada's process calculus. Third, we introduce a Kripke type semantics for a fragment of the logic, and show the completeness theorems with respect to the semantics. Finally, we mention a logic programming language based on the triple-context calculus. (shrink)

The paper introduces a first-order theory in the language of predicate tense logic which contains a single simple axiom. It is shewn that this theory enables times to be referred to and sentences involving ‘now’ and ‘then’ to be formalised. The paper then compares this way of increasing the expressive capacity of predicate tense logic with other mechanisms, and indicates how to generalise the results to other modal and tense systems.

Every truth-functional three-valued propositional logic can be conservatively translated into the modal logic S5. We prove this claim constructively in two steps. First, we define a Translation Manual that converts any propositional formula of any three-valued logic into a modal formula. Second, we show that for every S5-model there is an equivalent three-valued valuation and vice versa. In general, our Translation Manual gives rise to translations that are exponentially longer than their originals. This fact raises the question whether there are (...) three-valued logics for which there is a shorter translation into S5. The answer is affirmative: we present an elegant linear translation of the Logic of Paradox and of Strong Three-valued Logic into S5. (shrink)

The description of resources in game semantics has never achieved the simplicity and precision of linear logic, because of the misleading conception that linear logic is more primitive than game semantics. Here, we defend the opposite view, and thus advocate that game semantics is conceptually more primitive than linear logic. This revised point of view leads us to introduce tensor logic, a primitive variant of linear logic where negation is not involutive. After formulating its categorical semantics, (...) we interpret tensor logic in a model based on Conway games equipped with a notion of payoff, in order to reflect the various resource policies of the logic: linear, affine, relevant or exponential. (shrink)

This paper develops a modal, Sentential logic having "not", "if...Then" and necessity as logical constants. The semantics (system of meanings) of the logic is the most obvious generalization of the usual truth-Functional semantics for sentential logic and its deductive system (system of demonstrations) is an obvious generalization of a suitable (jaskowski-Type) natural deductive system for sentential logic. Let a be a set of sentences and p a sentence. "p is a logical consequence of a" is defined relative to the semantics (...) and "p is demonstrable from a" is defined relative to the deductive system. Main meta-Theorem: p is demonstrable from a if and only if p is a logical consequence of a. Henkin-Type methods are used. The theorems of the logic are exactly those of s5. The deductive system is rigorously developed as a system of linear strings. (shrink)

We consider the family of logics from NExt which are determined by linear frames with reflexive and symmetric relation of accessibility. The condition of linearity in such frames was first defined in the paper [9]. We prove that the cardinality of the logics under consideration is uncountably infinite.

ABSTRACT: This 1974 paper builds on our 1969 paper (Corcoran-Weaver [2]). Here we present three (modal, sentential) logics which may be thought of as partial systematizations of the semantic and deductive properties of a sentence operator which expresses certain kinds of necessity. The logical truths [sc. tautologies] of these three logics coincide with one another and with those of standard formalizations of Lewis's S5. These logics, when regarded as logistic systems (cf. Corcoran [1], p. 154), are seen to be equivalent; (...) but, when regarded as consequence systems (ibid., p. 157), one diverges from the others in a fashion which suggests that two standard measures of semantic complexity may not be as closely linked as previously thought. -/- This 1974 paper uses the linear notation for natural deduction presented in [2]: each two-dimensional deduction is represented by a unique one-dimensional string of characters. Thus obviating need for two-dimensional trees, tableaux, lists, and the like—thereby facilitating electronic communication of natural deductions. The 1969 paper presents a (modal, sentential) logic which may be thought of as a partial systematization of the semantic and deductive properties of a sentence operator which expresses certain kinds of necessity. The logical truths [sc. tautologies] of this logic coincides those of standard formalizations of Lewis’s S4. Among the paper's innovations is its treatment of modal logic in the setting of natural deduction systems--as opposed to axiomatic systems. The author’s apologize for the now obsolete terminology. For example, these papers speak of “a proof of a sentence from a set of premises” where today “a deduction of a sentence from a set of premises” would be preferable. 1. Corcoran, John. 1969. Three Logical Theories, Philosophy of Science 36, 153–77. J P R -/- 2. Corcoran, John and George Weaver. 1969. Logical Consequence in Modal Logic: Natural Deduction in S5 Notre Dame Journal of Formal Logic 10, 370–84. MR0249278 (40 #2524). 3. Weaver, George and John Corcoran. 1974. Logical Consequence in Modal Logic: Some Semantic Systems for S4, Notre Dame Journal of Formal Logic 15, 370–78. MR0351765 (50 #4253). (shrink)

In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). -/- The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is directly motivated in (...) terms of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising. (shrink)

A nonempty sequence T1,...,Tn of theories is tolerant, if there are consistent theories T 1 + ,..., T n + such that for each 1 i n, T i + is an extension of Ti in the same language and, if i n, T i + interprets T i+1 + . We consider a propositional language with the modality , the arity of which is not fixed, and axiomatically define in this language the decidable logics TOL and TOL. It is (...) shown that TOL (resp. TOL) yields exactly the schemata of PA-provable (resp. true) arithmetical sentences, if (A1,..., An) is understood as (a formalization of) PA+A1, ..., PA+An is tolerant. (shrink)

We investigate the expressivity of many-valued modal logics based on an algebraic structure with a complete linearly ordered lattice reduct. Necessary and sufficient algebraic conditions for admitting a suitable Hennessy–Milner property are established for classes of image-finite and modally saturated models. Full characterizations are obtained for many-valued modal logics based on complete BL-chains that are finite or have the real unit interval [0, 1] as a lattice reduct, including Łukasiewicz, Gödel, and product modal logics.

The present paper investigates the groups of automorphisms for some lattices of modal logics. The main results are the following. The lattice of normal extensions of S4.3, NExtS4.3, has exactly two automorphisms, NExtK.alt1 has continuously many automorphisms. Moreover, any automorphism of NExtS4 fixes all logics of finite codimension. We also obtain the following characterization of pretabular logics containing S4: a logic properly extends a pretabular logic of NExtS4 iff its lattice of extensions is finite and linear.

In this paper, we study temporal logic for finite linear structures and surjective bounded morphisms between them. We give a characterisation of such structures by modal formulas and show that every pair of linear structures with a bounded morphism between them can be uniquely characterised by a temporal formula up to an isomorphism. As the main result, we prove Kripke completeness of the logic with respect to the class of finite linear structures with bounded morphisms between them.

This paper investigates set-theoretical semantics for logics that contain unary connectives, which can be viewed as modalities. Indeed, some of the logics we consider are closely related to linear logic. We use insights from the relational semantics of relevance logics together with a new version of the squeeze lemma in our semantics for logics with disjunction. The ideal-based semantics, which takes co-theories to be situations, dualizes the theory-based semantics for logics with conjunction.

The Boolean many-valued approach to vagueness is similar to the infinite-valued approach embraced by fuzzy logic in the respect in which both approaches seek to solve the problems of vagueness by assigning to the relevant sentences many values between falsity and truth, but while the fuzzy-logic approach postulates linearly-ordered values between 0 and 1, the Boolean approach assigns to sentences values in a many-element complete Boolean algebra. On the modal-precisificational approach represented by Kit Fine, if a sentence is indeterminate in (...) truth value in some world, it is taken to be true in one precisified world accessible from that world and false in another. This paper points to a way to unify these two approaches to vagueness by showing that Fine’s version of the modal-precisificational approach can be combined with the Boolean many-valued approach instead of supervaluationism, one of the most popular approaches to vagueness. (shrink)

We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Došen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural (...) rules. With the exception of S5, the systems are modular in the sense that different structural rules capture different properties of the accessibility relation. We provide the first direct semantical cut-free completeness proofs for K, T, and D, and show how this method fails in the case of B and S4. (shrink)