Originally, I was going to use this writeup to describe what I thought were two unrelated meanings of the letter **K** in mathematics. However, after more research, I realised that the two meanings are in fact deeply and inextricably linked. More on that later; first, here are the two meanings.

In the early- to mid-20th century, mathematicians, for the first time, started to analyze the expressiveness and power of maths itself. In order to do this, they needed a model of computation which could then be used to reason about the very language it was expressed in. There were a number of different approaches, Alan Turing with his machines, Marvin Minsky with *his* machines, Andrei Markov with his algorithms but most importantly to us, Alonzo Church's Lambda calculus. Lambda calculus is basically a convenient way to express and apply functions. It was used to reason about computation where we only had functions available to us in our mathematical vocabulary.

Combinators are used as a set of basic functions in the lambda calculus, taken as given, so that more complex expressions can be written in terms of atomic building blocks. **K** is one of these combinators. Intuitively it accepts two arguments, ignores the second one and returns the first one. A few more formal descriptions:

or in

lambda calculus:

or in

ML:

fun K x y = x;

I have reservations giving C-style code due to the lack of type polymorphism.

Although this combinator seems incredibly simple and weedy, when used in conjunction with other combinators, such as **S**, and function application, it becomes very powerful.

In propositional logic, **K** is a standard axiom which a lot of proofs rely on.

Where → signifies inference.

This axiom can be shown to be valid from the truth table of the statements.

A | B | A → (B → A)
---+---+-------------
t | t | t
t | f | t
f | t | t
f | f | t

Again, this axiom seems obvious and useless. However, when combined with other axioms and Modus Ponens, **K** becomes an essential part of intuitionistic logic.

### The Connection

The similarity between the two **K**s became apparent when I was putting the ML code fragment into an interpreter. The type it gave for `fun K x y`

was

val K = fn : **'a -> 'b -> 'a**

The similarity between this and the logic axiom is striking

It turns out that this is no coincidence. A very deep result known as the Curry-Howard Isomorphism establishes direct correspondence between such seeminly diverse fields as second-order logic and polymorphic types, and importantly to us, minimal propositional logic and lambda calculus.

As the ML fragment given above is simply-typed lambda calculus in essence, it should be no surprise that there is such a direct connection between the **K** axiom and its related combinator's type.

**NB**, this does not mean that propositional logic is Turing complete, as lambda calculus is. It is the *types* of lambda expressions that are relevant, not the programmes themselves.