B, C, K, W system

Definition

• B x y z = x
• C x y z = x z y
• K x y = x
• W x y = x y y

• B x y z is the composition of the arguments x and y applied to the argument z;
• C x y z swaps the arguments y and z;
• K x y discards the argument y;
• W x y duplicates the argument y.

  Connection to other combinators

• B = S K
• C = S
• K = K
• W = S S

• I = W K
• K = K
• S = B = B .

  Connection to intuitionistic logic

• The implicational fragment of classical logic, would require the combinatory analog to the law of excluded middle, e.g., Peirce's law;
• Complete classical logic, would require the combinatory analog to the sentential axiom F → A.