BHK interpretation

In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey Kolmogorov. It is also sometimes called the realizability interpretation, because of the connection with the realizability theory of Stephen Kleene.

The interpretation states what is intended to be a proof of a given formula. This is specified by induction on the structure of that formula:

The interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of the formula s=t is a computation reducing the two terms to the same numeral.

Kolmogorov followed the same lines but phrased his interpretation in terms of problems and solutions. To assert a formula is to claim to know a solution to the problem represented by that formula. For instance ${\displaystyle P\to Q}$ is the problem of reducing Q to P; to solve it requires a method to solve problem Q given a solution to problem P.

The identity function is a proof of the formula ${\displaystyle P\to P}$, no matter what P is.

...
Wikipedia