or, in TPTP format: (1) fof(scharle1,axiom,![X]: t(s(X,s(X,X)))). (2) fof(scharle2,axiom,![X,Y,U,R]: t(s(s(X,s(Y,R)),s(s(s(U,Y),s(s(X,U),s(X,U))),s(s(U,Y),s(s(X,‌​U),s(X,U))))))).

Note: Scharle's two-basis contains a typo. Here is a sound and complete 2-axiom system, when combined with your weaker detachment rule (which Scharle calls D3): (1) DpDpp, (2) DDpDqrDDDsqDDpsDpsDDsqDDpsDps

yes, i suspect there is a single axiom for the weaker rule. i'll be working on this now.

note, also that Nicod's stronger rule also works with many other known axioms, including Lukaiewicz's. so, even if somehow this rule had worked with his axiom (in syntactically idiosyncratic way) it would still in this sense have been less generally useful than his stronger rule.

Right, sorry, thanks Andreas. I have fixed this above. Now a 4-element model is required. Note that t(•) is the theorem-hood predicate, and c1 = 0 is the instance of s(s(X,X)X) that fails to be a theorem. i.e., t(s(s(0,0),0)) = 0.