Kripke models for linear logic

1993 ◽  
Vol 58 (2) ◽  
pp. 514-545 ◽  
Author(s):  
Gerard Allwein ◽  
J. Michael Dunn
Keyword(s):  
Representation Theorem ◽  
Linear Logic ◽  
Kripke Model ◽  
Relevance Logic ◽  
Distributive Lattices ◽  
Kripke Models ◽  
Binary Operations ◽  
Modal Algebras ◽  
Boolean Lattices ◽  
Gaggle Theory

AbstractWe 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. Commutativity and associativity 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 residuated with Linear Logic's cotensor 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.

scholarly journals Priestley duality for MV-algebras and beyond

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Wesley Fussner ◽  
Mai Gehrke ◽  
Samuel J. van Gool ◽  
Vincenzo Marra
Keyword(s):  
Large Class ◽  
Order Conditions ◽  
Enriched Environment ◽  
Priestley Duality ◽  
Distributive Lattices ◽  
First Order ◽  
Dual Spaces ◽  
Binary Operations ◽  
New Perspective ◽  
Mv Algebras

Abstract We provide a new perspective on extended Priestley duality for a large class of distributive lattices equipped with binary double quasioperators. Under this approach, non-lattice binary operations are each presented as a pair of partial binary operations on dual spaces. In this enriched environment, equational conditions on the algebraic side of the duality may more often be rendered as first-order conditions on dual spaces. In particular, we specialize our general results to the variety of MV-algebras, obtaining a duality for these in which the equations axiomatizing MV-algebras are dualized as first-order conditions.

Multiplicative conjunction and an algebraic meaning of contraction and weakening

1998 ◽  
Vol 63 (3) ◽  
pp. 831-859 ◽  
Author(s):  
A. Avron
Keyword(s):  
Classical Logic ◽  
Linear Logic ◽  
Substructural Logics ◽  
Interesting Property ◽  
Relevance Logic ◽  
Proper Subset ◽  
Algebraic Structures ◽  
Elimination Rule ◽  
First Case ◽  
Soundness And Completeness

AbstractWe show that the elimination rule for the multiplicative (or intensional) conjunction Λ is admissible in many important multiplicative substructural logics. These include LLm (the multiplicative fragment of Linear Logic) and RMIm (the system obtained from LLm by adding the contraction axiom and its converse, the mingle axiom.) An exception is Rm (the intensional fragment of the relevance logic R, which is LLm together with the contraction axiom). Let SLLm and SRm be, respectively, the systems which are obtained from LLm and Rm by adding this rule as a new rule of inference. The set of theorems of SRm is a proper extension of that of Rm, but a proper subset of the set of theorems of RMIm. Hence it still has the variable-sharing property. SRm has also the interesting property that classical logic has a strong translation into it. We next introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLLm relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLLm corresponds to the condition that there will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element (in the first case we get the system BCKm, in the second - the system SRm). Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts.

scholarly journals Subdirect products of rings and distributive lattices

1982 ◽  
Vol 25 (2) ◽  
pp. 155-171 ◽  
Author(s):  
Hans-J. Bandelt ◽  
Mario Petrich
Keyword(s):  
Unary Operation ◽  
General Construction ◽  
Distributive Lattices ◽  
Identity Mapping ◽  
Additive Subgroup ◽  
Binary Operations ◽  
Subdirect Products

Rings and distributive lattices can both be considered as semirings with commutative regular addition. Within this framework we can consider subdirect products of rings and distributive lattices. We may also require that the semirings with these restrictions are regarded as algebras with two binary operations and the unary operation of additive inversion (within the additive subgroup of the semiring). We can also consider distributive lattices with the two binary operations and the identity mapping as the unary operation. This makes it possible to speak of the join of ring varieties and distributive lattices. We restrict the ring varieties in order that their join with distributive lattices consist only of subdirect products. In certain cases these subdirect products can be obtained via a general construction of semirings by means of rings and distributive lattices.

Sufficient conditions for the undecidability of intuitionistic theories with applications

1972 ◽  
Vol 37 (2) ◽  
pp. 375-384 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Decision Problem ◽  
Sufficient Conditions ◽  
Kripke Model ◽  
The Other ◽  
Predicate Calculus ◽  
Kripke Models ◽  
Symmetric Relation ◽  
Undecidable Theory ◽  
Classical Models ◽  
Classical Predicate

Let Δ be a set of axioms of a theory Tc(Δ) of classical predicate calculus (CPC); Δ may also be considered as a set of axioms of a theory TH(Δ) of Heyting's predicate calculus (HPC). Our aim is to investigate the decision problem of TH(Δ) in HPC for various known theories Δ of CPC.Theorem I(a) of §1 states that if Δ is a finitely axiomatizable and undecidable theory of CPC then TH(Δ) is undecidable in HPC. Furthermore, the relations between theorems of HPC are more complicated and so two CPC-equivalent axiomatizations of the same theory may give rise to two different HPC theories, in fact, one decidable and the other not.Semantically, the Kripke models (for which HPC is complete) are partially ordered families of classical models. Thus a formula expresses a property of a family of classical models (i.e. of a Kripke model). A theory Θ expresses a set of such properties. It may happen that a class of Kripke models defined by a set of formulas Θ is also definable in CPC (in a possibly richer language) by a CPC-theory Θ′! This establishes a connection between the decision problem of Θ in HPC and that of Θ′ in CPC. In particular if Θ′ is undecidable, so is Θ. Theorems II and III of §1 give sufficient conditions on Θ to be such that the corresponding Θ′ is undecidable. Θ′ is shown undecidable by interpreting the CPC theory of a reflexive and symmetric relation in Θ′.

Finite Kripke models and predicate logics of provability

1990 ◽  
Vol 55 (3) ◽  
pp. 1090-1098 ◽  
Author(s):  
Sergei Artemov ◽  
Giorgie Dzhaparidze
Keyword(s):  
Modal Logic ◽  
Kripke Model ◽  
Finite Model ◽  
Kripke Models ◽  
Model Property ◽  
Logical Formula ◽  
Finite Model Property ◽  
Modal Predicate Logics ◽  
The One ◽  
Arithmetical Interpretation

AbstractThe paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic:If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that PA ⊬ fR.This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding “the predicate part” as a specific addition to the standard Solovay construction.

scholarly journals Intrusion detection system episteme

2012 ◽  
Vol 2 (3) ◽  
Author(s):  
Daniel Mihályi ◽  
Valerie Novitzká ◽  
Martina Ľaľová
Keyword(s):  
Intrusion Detection ◽  
Intrusion Detection System ◽  
Detection System ◽  
Linear Logic ◽  
Kripke Model ◽  
Modal Logics ◽  
Simplified Model

AbstractIn our paper we investigate the possibilities of modal logics in coalgebras of program systems. We deal with a simplified model of an intrusion detection system. We model an intrusion detection system as a coalgebra and construct its Kripke model of coalgebraic modal linear logic using powerset endofunctor. In this model we present our idea how a fragment of epistemic linear logic can provide knowledge and belief of intrusion attempt.

On categorical models of classical logic and the Geometry of Interaction

2007 ◽  
Vol 17 (5) ◽  
pp. 957-1027 ◽  
Author(s):  
CARSTEN FÜHRMANN ◽  
DAVID PYM
Keyword(s):  
Classical Logic ◽  
Disjoint Union ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Structural Theory ◽  
Cut Elimination ◽  
Categorical Models ◽  
Boolean Lattices ◽  
Deep Exploration ◽  
Straightforward Proof

It is well known that weakening and contraction cause naive categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarised briefly herein, we have provided a class of models calledclassical categoriesthat is sound and complete and avoids this collapse by interpreting cut reduction by a poset enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product. In this article, which is self-contained, we present an improved axiomatisation of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models calledDummett categories. Examples of these include, besides the classical categories mentioned above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices, which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic by applying it to obtain a classical category from a Dummett category.Along the way, we gain detailed insights into the changes that proofs undergo during cut elimination in the presence of weakening and contraction.

scholarly journals Stone Lattices

2015 ◽  
Vol 23 (4) ◽  
pp. 387-396 ◽  
Author(s):  
Adam Grabowski
Keyword(s):  
Lattice Theory ◽  
Cartesian Product ◽  
Unary Operation ◽  
Binary Operations ◽  
Pseudocomplemented Lattice ◽  
Stone Lattice ◽  
Current Article ◽  
Boolean Lattices ◽  
Pseudocomplemented Lattices ◽  
Natural Way

Summary The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the paper, the notion of a pseudocomplement in a lattice is formally introduced in Mizar, and based on this we define the notion of the skeleton and the set of dense elements in a pseudocomplemented lattice, giving the meet-decomposition of arbitrary element of a lattice as the infimum of two elements: one belonging to the skeleton, and the other which is dense. The core of the paper is of course the idea of Stone identity $$a^* \sqcup a^{**} = {\rm{T}},$$ which is fundamental for us: Stone lattices are those lattices L, which are distributive, bounded, and satisfy Stone identity for all elements a ∈ L. Stone algebras were introduced by Grätzer and Schmidt in [18]. Of course, the pseudocomplement is unique (if exists), so in a pseudcomplemented lattice we defined a * as the Mizar functor (unary operation mapping every element to its pseudocomplement). In Section 2 we prove formally a collection of ordinary properties of pseudocomplemented lattices. All Boolean lattices are Stone, and a natural example of the lattice which is Stone, but not Boolean, is the lattice of all natural divisors of p 2 for arbitrary prime number p (Section 6). At the end we formalize the notion of the Stone lattice B [2] (of pairs of elements a, b of B such that a ⩽ b) constructed as a sublattice of B 2, where B is arbitrary Boolean algebra (and we describe skeleton and the set of dense elements in such lattices). In a natural way, we deal with Cartesian product of pseudocomplemented lattices. Our formalization was inspired by [17], and is an important step in formalizing Jouni Järvinen Lattice theory for rough sets [19], so it follows rather the latter paper. We deal essentially with Section 4.3, pages 423–426. The description of handling complemented structures in Mizar [6] can be found in [12]. The current article together with [15] establishes the formal background for algebraic structures which are important for [10], [16] by means of mechanisms of merging theories as described in [11].

scholarly journals Simple and subdirectly irreducibles bounded distributive lattices with unary operators

2006 ◽  
Vol 2006 ◽  
pp. 1-20 ◽  
Author(s):  
Sergio Arturo Celani
Keyword(s):  
Distributive Lattices ◽  
Heyting Algebras ◽  
Subdirectly Irreducible ◽  
Modal Algebras ◽  
Heyting Algebras With Operators ◽  
Subdirectly Irreducibles ◽  
Subdirectly Irreducible Algebras

We characterize the simple and subdirectly irreducible distributive algebras in some varieties of distributive lattices with unary operators, including topological and monadic positive modal algebras. Finally, for some varieties of Heyting algebras with operators we apply these results to determine the simple and subdirectly irreducible algebras.

Sign in / Sign up

Export Citation Format

Share Document