B,C,K,W System - Connection To Intuitionistic Logic

Connection To Intuitionistic Logic

The combinators B, C, K and W correspond to four well-known axioms of sentential logic:

AB: (B → C) → ((A → B) → (A → C)),
AC: (A → (B → C)) → (B → (A → C)),
AK: A → (B → A),
AW: (A → (A → B)) → (A → B).

Function application corresponds to the rule modus ponens:

MP: from A and A → B infer B.

The axioms AB, AC, AK and AW, and the rule MP are complete for the implicational fragment of intuitionistic logic. In order for combinatory logic to have as a model:

• 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.