Sistema B, C, K, W
# Sistema B, C, K, W

El sistema B, C, K, W es una variante de lógica combinatoria que toma como primitivas a los combinadores B, C, K, y W. Este sistema fue propuesto originalmente por el matemático estadounidense Haskell Curry en su tesis doctoral Grundlagen der kombinatorischen Logik (Fundamentos de la lógica combinatoria).

## Definición

Los combinadores se definen como sigue:

* B x y z = x (y z)
* C x y z = x z y
* K x y = x
* W x y = x y y

De forma intuitiva,

* B x y z es la composición de los argumentos x e y aplicada al argumento z;
* C x y z intercambia los argumentos y y z;
* K x y descarta el argumento y;
* W x y duplica el argumento y.

## Conexión con otros combinadores

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 pueden expresarse en términos de S y K como sigue:

* B = S (K S) K
* C = S (S (K (S (K S) K)) S) (K K)
* K = K
* W = S S (S K)

En la otra dirección, SKI puede definirse en términos de B, C, K, W como:

* I = W K
* K = K
* S = B (B (B W) C) (B B) = B (B W) (B B C).

## Conexión con la lógica intuicionista

Los combinadores B, C, K y W corresponden a cuatro conocidos axiomas de la lógica proposicional:

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

La aplicación de la función corresponde a la regla modus ponens:

    MP: de A y A → B infiere B.

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:

* El fragmento implicacional de la lógica clásica, requeriría el análogo combinatorio al principio del tercero excluido, por ejemplo, la ley de Peirce;
* La lógica clásica completa, requeriría el análogo combinatorio al axioma sentencial F → A.
