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 combinador SKI , con sólo 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 anteriormente, definir con más detalle C = S ( BBS ) ( KK ) y W = CSI .
En la otra dirección, SKI se puede definir en términos de B, C, K, W como:
También es de 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 oracional :
La aplicación de la función corresponde a la regla modus ponens :
Los axiomas AB , AC , AK y AW , y la regla MP están completos para el fragmento implicacional de la lógica intuicionista . Para que la lógica combinatoria tenga como modelo: