 Now Curry’s work in (1934) and more fully with Feys in (1958) had shown a certain correspondence between provable formulae in the theory of the conditional and the types of basic combinators in type theory. In particular, with \(\rightarrow\) as the conditional and \(\alpha \Rightarrow \beta\) representing function types, that is types (construed non-syntactically) whose inputs are type \(\alpha\) functions and outputs type \(\beta\) functions, we have, (here \(\vdash_{T\rightarrow}\) means provability in the positive (non-relevantist) theory of the conditional and \(\vdash_{CL}\) means provability in a suitable combinatory logic): 