Abstract

In [3] the prepositional connectives were defined in terms of the combinators K and S and the illative obs Ξ and H . Given an elimination rate for Ξ and introduction rules for H and Ξ, all the standard intuitionistic propositional calculus results could be proved provided the variables were restricted to H. The intuition behind the particular introduction rule for Ξ of [2], that was used is [3], came from a three valued truth table for implication, the values of which were T, F and N. . There are in fact 4 different truth tables for implication that fit the rules for implication derived from those for Ξ. From these 4 different tables for conjunction and two for disjunction can be derived