B,C,K,Wシステム
定数記号 B, C, K, W はそれぞれよく知られた4つの命題論理の公理と対応する:
AB: (B → C) → ((A → B) → (A → C)),
AC: (A → (B → C)) → (B → (A → C)),
AK: A → (B → A),
AW: (A → (A → B)) → (A → B).
関数適用はモーダスポネンスに対応する:
MP: A → B , A ⊢ B {\displaystyle A\to B,A\vdash B}
公理 AB, AC, AK, AW 及び推論規則 MP は、直観主義命題論理の含意断片(英語版)に対して完全である。この体系に爆発原理 F → A と排中律に類する規則(例:パースの法則)を加えたものは古典命題論理と対応する。コンビネータ W とそれに関する公理図式を取り除いたものはBCK論理と対応する。これはBCK-λ計算と対応するものである。