> 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...
A positive answer to QUESTION V (https://web.ics.purdue.edu/~dulrich/Twenty-six-open-question...) would seem to mean λx. x B K is as short as possible.