Grishin algebras and cover systems for classical bilinear logic (Q647406)

The aim of the paper is to show a construction of Grishin algebras based on certain subsets of cover systems with an orthogonality relation used to interpret the negations. In order to achieve this aim, first it is shown that the Grishin algebras are closed under MacNeille completion. Using this fact the author proves the main result of the paper saying that an arbitrary Grishin algebra has an isomorphic embedding into the algebra of all propositions of some cover system, by a map that preserves all existing joins and meets. The paper is completed by a presentation of a cover system semantics for a version of classical bilinear logic that has first-order quantifiers and infinitary conjunctions and disjunctions.