Regarding http://jwodder.freeshell.org/lambda.html http://jwodder.freeshell.org/lambda.html, "B" is Hypothetical Syllogism (transitivity of implication (the "ma

Regarding http://jwodder.freeshell.org/lambda.html http://jwodder.freeshell.org/lambda.html, "B" is Hypothetical Syllogism (transitivity of implication (the "material conditional")), which is the composition of the arguments x and y applied to the argument z (https://en.wikipedia.org/wiki/B,_C,_K,_W_system https://en.wikipedia.org/wiki/B,_C,_K,_W_system) rather than the composition of the arguments x and y alone. > where I look for the shortest way, the simplest way, the "first principles", for example to build the numbers, the operators Since the "conditional's" or implication's elimination (application-"MP"), introduction (abstraction) & distributivity axioms ("K" & "S") in addition to first binding a "hypothesis" or (free) variable "x", which is "f" in the "Iota" definition, leads to the "X" single combinator/axiom, and since "S" may be derived from ("B":local consistency) & ("K":local completeness or η-reduction (eta reduction) or extensionality) this leads to the shorter locally indecisive single aXiom definition := λx. x B K Meredith first found a form of the shortest definition and others have been listed by the now deceased Dolph Ulrich: https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page... A positive answer to QUESTION V (https://web.ics.purdue.edu/~dulrich/Twenty-six-open-questions-page.htm https://web.ics.purdue.edu/~dulrich/Twenty-six-open-question...) would seem to mean λx. x B K is as short as possible.