CONJUNCTION WITHOUT CONDITIONS IN ILLATIVE COMBINATORY LOGIC
Martin W. Bunder · 2008
In [3] the prepositional connectives were defined in terms of the combinators K and S and the illative obs Ξ and H (ΞXY can be interpreted as “Y V holds for all V such that XV holds” and HX can be interpreted as “X is a proposition”). 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 . (N can be read as “nonsignificant” or “not T nor F”). 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 (∨) (as well as one for negation and one for H) can be derived (see [4]). The introduction and elimination rules for the connectives derived from the postulates for Ξ and H, where, with some exceptions, the most general ones that would fit all the truth tables. The exceptions were the elimination rules for ∧ and ∨ which came out as: