Some lattice models of bilinear logic (Q1906000): Difference between revisions

Bilinear logic is treated in the paper as a logic without the three Gentzen structural rules: interchange, weakening and contraction. It is a non-commutative version of linear logic which allows two negations. Only classical propositional bilinear logic is actually considered. The author aims at presenting the class of Grishin algebras, generalizations of Boolean algebras that serve as models of bilinear logic. A Grishin algebra is essentially a residuated lattice-ordered monoid with two additional unary operations (negations). Some elementary properties of Grishin algebras are described. In particular, the lattice \(L(G)\) of downward closed subsets of a Grishin algebra \(G\) is again a Grishin algebra. It is shown that if \(G\) has certain special properties, then the two negation operations on \(L(G)\) are distinct.