Kripke semantics for logics with BCK implication

We present Kripke semantics for some substructural logics with weakening, known as logics with BCK implication. This work is a continuation of the work of Allwein and Dunn on Kripke semantics for Linear Logic, which in turn rested on Dunn's Gaggle Theory and on Urquhart's Representation Theory for nondistributive lattices. The basic idea in the representation theory is to use maximally disjoint filter-ideal pairs (maximal pairs) to separate distinct elements. A collection of subsets of the set of maximal pairs forms the representation lattice. Ternary relations are defined on the set of maximal pairs which embody properties of the operations and and : A three way valuation of formulas gives rise to a definition of canonical Kripke model. Properties of the ternary relations on the set of maximal pairs are used in the abstract definition of Kripke semantics. Soundness and strong completeness hold.