El sistema B, C, K, W es una variante de la lógica combinatoria que toma como primitivos los combinadores B, C, K y W. Este sistema fue descubierto por Haskell Curry en su tesis doctoral Grundlagen der kombinatorischen Logik , cuyos resultados se exponen en Curry (1930).
Los combinadores se definen de la siguiente manera:
Intuitivamente,
En las últimas décadas, el cálculo combinatorio SKI , con solo dos combinadores primitivos, K y S , se ha convertido en el enfoque canónico de la lógica combinatoria . B, C y W se pueden expresar en términos de S y K de la siguiente manera:
Otra forma es, habiendo definido B como arriba, definir además C = S ( BBS )( KK ) y W = CSI .
Yendo en la otra dirección, SKI se puede definir en términos de B, C, K, W como:
También cabe destacar que el combinador Y tiene una expresión corta en este sistema, como Y = BU ( CBU ), donde U = WI = SII es el combinador de autoaplicación. Entonces tenemos Y g = U ( B g U ) = B g U ( B g U ) = g( U ( B g U )) = g( Y g).
Los combinadores B , C , K y W corresponden a cuatro axiomas bien conocidos de la lógica sentencial :
La aplicación de la función corresponde a la regla modus ponens :
Los axiomas AB , AC , AK y AW , y la regla MP son completos para el fragmento implicacional de la lógica intuicionista . Para que la lógica combinatoria tenga como modelo: