Bisimulation is the basic equivalence between models in modal logic. Although bisimulation implies modal equivalence, the converse does not hold in general. Hennessy–Milner-style theorems find various conditions under which the converse holds, e.g. finiteness. In Kripke semantics, the condition of finiteness can be improved to image-finiteness, i.e., a model may be infinite, but without infinite branching. The present paper proposes local finiteness as an analogue of this property for topological semantics, proves appropriate Hennessy–Milner theorem analogues, and shows how locally finite topologies, in fact, directly correspond to image-finite Kripke models.
In the article we discuss the notion of a subnormal modal logic and, in particular, the notion of an intermediate subnormal modal logic. The goal of the article is to determine the cardinality of the set of all intermediate subnormal modal logics. Thus we define a set of certain formulas, such that each subset of the defined set determines a different intermediate subnormal modal logic. As we demonstrate, since the set in question is countable, the set of all intermediate subnormal modal logics has cardinality of the continuum.
GE-algebras are introduced as a generalization of Hilbert algebras in 2020. In this paper, we show that a self distributive GE-algebra is equivalent to the pimpl-RML algebra, and a transitive GE algebra is equivalent to the pi-pre-BBBCC algebra with condition (An). Further, we prove that pimpl-BE algebras are a subclass of pimpl-RML algebras and pre-Hilbert algebras with condition (GE3) are equivalent to the pi-pre-BBBCC algebras with condition (An).
In this paper, we introduce the notion of double equivalential algebras, defined as subreducts of double Heyting algebras with respect to the equivalence and dual equivalence operations. We establish the fundamental properties of these structures and investigate several distinguished classes related to them, including the class of double equivalential subreducts of Boolean algebras and the variety generated by the three-element chain, which is shown to be semisimple.
In this paper, inspired by the concepts of the radical of an ideal and the Jacobson radical in ring theory, we introduce these notions in the context of L-algebras. Our main goal is to explore the nature of the radical of an ideal and Jacobson radical in specific L-algebras. We successfully identify the elements of these radicals in special classes of L-algebras, including proper Glivenko algebras and finite Brouwerian semi-lattices using a closure operator. To achieve this goal, we introduce a new notion that is associated with any element a ∈ L as well as with an ideal of an L-algebra L.
In this paper, by special upsets on equality algebras, we construct a topology on bounded equality algebras and investigate some of their topological properties, such as Hausdorff, T0-space, T1-space and disconnected. In addition, we express the relation between closed and compact sets in this topology. Moreover, by considering the binary operation ↠ and constructing a topology on the bounded equality algebra E, we introduce the notion of semi-topological algebra and prove that any involutive equality algebra is a right semi-topological algebra and by some conditions it can be a semi-⋏-topological algebra. Also, we show that it is not necessarily a left semi-topological algebra. Finally, we investigate converse image, product and quotient topology on equality algebra and show that under what condition we can make finer topology.
In this article, a specific type of semi maximal filters is introduced, which form a lattice structure. These filters are called J- semi maximal and NJ-semi maximal, and their key properties in BL-algebras are analyzed. Additionally, these special filters are compared with other defined filters, particularly semi maximal and maximal filters. The purpose of this article is to provide a new analysis of filters in BL-algebras.
In this paper we consider the Intuitionistic Sentential Calculus with Identity (ISCI). We study two main families of sequent calculi. The first one, called G3ISCI, is based on a label-free multi-succedent sequent calculus that is sound and complete w.r.t. Kripke models and the second, called L3ISCI, is based on a multi-succedent labeled sequent calculus that is sound and complete w.r.t. Beth models. Our goal is to investigate how the calculi, that capture distinct semantics of the logic, relate to each other through proof translations. Proof translations from G3ISCI to L3ISCI provide new results about the soundness and (cut-free) completeness of G3ISCI w.r.t. Beth models. Proof translations from L3ISCI to G3ISCI are more difficult and require the definition of new calculi for ISCIthat provide intermediate steps in the translation process.
We prove that the modal logic of lattices with the accessibility relation of being isomorphic to a sublattice is S4.2. The same is proven for modular and distributive lattices.
It is well established that classical propositional logic is Boolean. However, this view has recently been challenged. In their paper Non-Orthomodular Models for Both Standard Quantum Logic and Standard Classical Logic: Repercussions for Quantum Computers, Mladen Pavic̆ić and Norman Megill present a non-distributive, non-orthomodular model for both classical and quantum logic based on lattice O6, and argue that classical propositional logic is non-distributive. In this paper, we examine this claim. Pavic̆ić and Megill’s model is formulated within unital matrix semantics rather than as an algebraic model in the sense of Abstract Algebraic Logic. An analysis of the lattice O6 in the framework of matrix semantics reveals that the matrix (O6,{1,a,b}) is adequate for CL, but not reduced, and induces the same consequence relation as the two-element Boolean matrix B2. Similarly, the unital matrix (O6,{1}) is adequate for CL through reduction to the four-element Boolean matrix B4. Furthermore, we present two lattice constructions that yield matrix models for CL lacking nontrivial lattice-theoretic properties. These results show that the adequacy of O6 is not intrinsic to its algebraic structure, but is inherited from its reducibility to Boolean matrices, and more generally that classical logic admits models with highly unconstrained lattice structure. Consequently, the existence of such non-distributive models does not undermine the distributive character of classical propositional logic.
A. V. Figallo introduced the 3-valued Super Łukasiewicz logic expanded with the Δ operator, denoted as C3↣,Δ, in 1990. This operator is used in the definition of 3-valued Łukasiewicz algebras, and it is not possible to recover Δ through implication and top in Super Łukasiewicz logic. On the other hand, Baaz introduced the Δ operator in Gödel logic, both in its propositional and quantified versions. Subsequently, this operator was extensively studied in the field of fuzzy logic. In this paper, we prove a strong version of the Adequacy Theorem for C3↣,Δ3. As a consequence, we demonstrate that the Deduction Theorem does not hold in this calculus. Furthermore, we introduce the first-order version of C3↣,Δ3 and establish soundness and completeness results by adapting a recently developed algebraic technique. In this context, our presentation differs from others in the literature because we need to construct a special homomorphism, brought from the algebraic study of C3↣,Δ3, in the syntactic setting. This homomorphism is also necessary to determine the generating algebras. While we can ascertain that the logical system is algebraizable by a (quasi-)variety of algebras, we cannot know a priori which are the subdirectly irreducible algebras.
We develop the theory of residuated lattices by introducing and studying several new types of filters and related concepts, including semi-simple filters, essential filters, the socle of a filter, and independent families of filters. Our primary goal is to understand the inner structure of residuated lattices by analyzing these new objects. First, we establish the key properties of simple and essential filters. Next, we then provide both algebraic and topological characterizations for identifying when a filter is simple or essential. Furthermore, we use the concepts of the socle and independent families to delve deeper into the structure of filters and the residuated lattice itself. We also provide several characterizations for semi-simple filters and residuated lattices. A central result shows that for finite residuated lattices, being semi-simple is equivalent to being hyperarchimedean, highlighting the natural connection between these concepts. Complementary results deepening on the understanding of the relation between simple filters and maximal filters in residuated lattices are also established.
The Nonassociative Lambek Calculus (NL) represents a logic devoid of the structural rules of exchange, weakening, and contraction, and it does not presume the associativity of its connectives. Its finitary consequence relation is decidable in polynomial time. However, the addition of classical connectives conjunction and disjunction (FNL) makes the consequence relation undecidable. Interestingly, if these connectives are distributive, the consequence relation is decidable in exponential time. This paper provides the proof, that we can merge classical logic with NL (i.e. BFNL) and intuitionistic logic with NL (i.e. HFNL), and still consequence relations are decidable in exponential time.
According to Russell, the definite article 'the' in a definite description 'the F' is used strictly in case there is a unique F and it is used loosely in case there is more than one F. Russell's analysis of constructions of the form 'the F is G' is concerned only with the strict use. We modify this analysis so as to allow also for the loose use. This is achieved essentially by replacing the usual undefined notion of identity in Russell's uniqueness clause with the defined notion of qualified identity (i.e., 'a is the same as b in all 2-respects', where 2 is a subset of the set of predicate constants P) proposed in earlier work. This modification gives us qualified notions of uniqueness and definiteness. A qualified definiteness statement 'the 2-unique F is G' is strict in case 2 = P and loose in case 2 is a proper subset of P. The account is made formally precise in terms of proof theory and proof-theoretic semantics. The framework is intended to be acceptable from a foundational intuitionistic point of view. It is applied to natural language constructions with complete, incomplete, and generic definite descriptions. Also constructions with nested and with predicatively used definite descriptions are considered as well as constructions involving possessives. This work incorporates and extends my NCL'24-paper 'Incomplete descriptions and qualified definiteness'.
This work studies the proof theory and ternary relational semantics of left (right) skew monoidal closed categories and skew monoidal bi-closed categories, both symmetric and non-symmetric, from the perspective of non-associative Lambek calculus. Uustalu et al. used sequents with stoup (the leftmost position of an antecedent that can be either empty or a single formula) to deductively model left skew monoidal closed categories, yielding results regarding proof identities and categorical coherence. However, their syntax does not work well when modeling right skew monoidal closed and skew monoidal bi-closed categories, whether symmetric or non-symmetric. We solve the problem via more flexible and equivalent frameworks to characterize the categories above: tree sequent calculus (where antecedents are binary trees) and axiomatic calculus (where antecedents are a single formula), inspired by works on non-associative Lambek calculus. Moreover, we prove that the axiomatic calculi are sound and complete with respect to their ternary relational models. We also prove a correspondence between frame conditions and structural laws, providing an algebraic way to understand the relationship between the left and right skew monoidal closed categories, encompassing both symmetric and non-symmetric variants.
A unified Gentzen-style proof-theoretic framework for until-free propositional linear-time temporal logic and its intuitionistic variant is introduced. The framework unifies Gentzen-style single-succedent sequent calculi and natural deduction systems for both the classical and intuitionistic versions of these temporal logics. Theorems establishing the equivalence between the proposed sequent calculi and natural deduction systems are proved. Furthermore, the cut-elimination theorems for the proposed sequent calculi and the normalization theorems for the proposed natural deduction systems are established.
Ecumenical logics are systems where two logics can coexist, sharing vocabulary and avoiding collapses between them. The literature has focused mainly on ecumenism between classical and intuitionistic logic, and several calculi of Natural Deduction and Sequents have been proposed. In this paper I contribute to this project with a dialogical ecumenical system. This Game utilizes an extension of the intuitionistic structural rules that permits to handle classical disjunctions and conditionals. I show that this is indeed an ecumenical dialogical system, where classical formulas and intuitionistic formulas can be validated without collapses between them, and provide a philosophical defense of its design.
We introduce the concepts of dually balanced lattices and \(M\)-lattices and provide some basic properties of these classes of lattices. Both classes can be viewed as generalizations of the well-known class of modular lattices. In particular, we obtain analogues of the Kurosh-Ore theorem for dually balanced lattices and the Jordan-Hölder theorem for \(M\)-lattices. Furthermore, we investigate the behaviour of several invariants, including the hollow dimension and the Kurosh-Ore dimension in dually balanced lattices, as well as the maximal dimension in \(M\)-lattices.
In this paper, involutive weak exchange algebras (for short, involutive WE al gebras) are introduced and studied. Their properties and characterizations are investigated. Some important results and examples are given. In particular, it is proven that in involutive WE algebras, the properties (BB), (B), (*), (**) and (Tr) are equivalent. Moreover, involutive BE, involutive GE, involutive pre-BCK and involutive pre-Hilbert algebras are considered, their connections are established. It is shown that involutive WE algebras (respectively, involutive GE algebras) satisfying the commutative property are Wajsberg algebras (respec tively, Boolean algebras). Finally, the interrelationships between the classes of involutive algebras considered here are presented.
