title: Sistema B, C, K, W
text: # 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).
  
  # Sistema B, C, K, W
  ## 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.
  
  # Sistema B, C, K, W
  ## 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).
  
  # Sistema B, C, K, W
  ## 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.