Propositional and predicate calculuses based on combinatory logic.
Martin W. Bunder · Notre Dame Journal of Formal Logic · 1974
In this article we shall establish various propositional and predicate calculuses based on combinatory logic (see [4]) with suitable restrictions on the variables.These restrictions are needed to avoid Curry's paradox ([4] pp.258, 259).We require, Rule H, the rule of restricted generality: axy, xu \-yu, and the iterated deduction theorem for Ξ. 1 // X 09 X ίy . . ., X m y-Y where no u k occurs in any Xj for j y H(* D y),we obtain all of the absolute (or intuitionistic) calculus of pure implication.If we then introduce a slightly more complex axiom connecting Ξ and H, 1.In [2] L was defined as FAH or B(ΞA(BH)) and HX was interpreted as α X is a proposition."Here however we take L as primitive and define H by BLK.If we have L = FAH and H primitive, we need either Axiom 2 or Axiom 8 (HLA) of [2] to prove Theorem 3 below.Xu Z) u Yu stands for BXY.Note that this form of the deduction theorem avoids the Kleene-Rosser paradox (See [3]).