[FOM] Defining implication on non-distributive lattices

[CGMcKay]

After a very long break from logic, I recently had reason to look at certain systems for so-called quantum logic and this led me subsequently to reflect more generally on the problem of defining implication (>) on non-distributive lattices. In view of the familiar difficulties, my idea was the following. Consider the formulation of intuitionist propositional logic to be found in Kleene's Introduction to Metamathematics. Retain all the axioms for implication, disjunction and negation but in the case of conjunction keep (a&b)>a and (a&b)>b but drop the axiom (a>(b>(a&b))) and instead extend the rules of inference by supplementing MP with the rule (WC) if  we have (F>G) is PROVABLE and (F>H) is PROVABLE then (F>G&H) is PROVABLE. Call the resulting system Weak Conjunction. It then becomes possible to define > on any lattice with 0 and 1 (represent > by the binary "order function" on L where f(xy)=1 if x is less than or equal to y and y otherwise) so that all the theorems of Weak Conjunction are valid on L. Although Weak Conjunction is manifestly weaker than intutionist propositional logic with regard to theorems containing the connective &, we have at the same time the following  'translation metatheorem': every word F in which conjunction occurs can be translated into an intuitionistically equivalent word t(F) which is a conjunction of conjunction-free words and we have that F is provable in intuitionist propositional logic iff t(F) is provable in Weak Conjunction. This embedding can then be extended to classical logic via Glivenko so that F is provable in classical logic iff t(double neg F) is provable in weak conjunction. Now two problems. (1) is the system of Weak Conjunction decidable? (Obviously the implication-disjunction-negation fragment is) (2) for non-distributive lattices, is there some interpretation of implication distinct from the "order function" which makes all the theorems of Weak Conjunction valid? Incidentally the order-function interpretation is not faithful to intuitionist intentions since it also validates (((a>b)>b)v(a>b)) and thus also (neg a v double neg a). Any input from FOM list members would be much appreciated. Craig (C.G.McKay).