© 1997 by Oxford University Press
Combinators and structurally free logic
Departments of Philosophy and Computer Science, Indiana University, Bloomington, IN 47405, USA A1 Automated Reasoning Project, The Australian National University, Canberra, ACT 2604, Australia
A 'Kripke-style' semantics is given for combinatory logic using frames with a ternary accessibility relation, much as in the Tourley-Meyer semantics for relevance logic. We prove by algebraic means a completeness theorem for combinatory logic, by proving a representation theorem for 'combinatory posets.' A philosophical interpretation is given of the models, showing that an element of a combinatory poset can be understood simultaneously as a set of states and as a set of (untyped) actions on states. This double interpretation allows for one such element to be applied to another (including itself). Application turns out to be modeled the same way as 'fusion' in relevance logic.
We also introduce 'dual combinators' that apply from the right. We then explore relationships to some well-known substructural logics, showing that each can be embedded into the structurally free. non-associative Lambek calculus, with the embedding taking a theorem 
to a statement of the form 
, where is some fusion of the combinators (sometimes dual combinators as well) needed to justify the structural assumptions of the given substructural logic. This builds on earlier ideas from Belnap and Meyer about a Gentzen system wherein structural rules are replaced with rules for introducing combinators. We develop such a system and prove a cut theorem.
Keywords: combinatory logic, substructural logic, Gentzen, gaggle, relevance logic, semantics, algebraic logic