In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, is an explanation of the meaning of proof in
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
, proposed by
L. E. J. Brouwer and
Arend Heyting, and independently by
Andrey Kolmogorov
Andrey Nikolaevich Kolmogorov ( rus, Андре́й Никола́евич Колмого́ров, p=ɐnˈdrʲej nʲɪkɐˈlajɪvʲɪtɕ kəlmɐˈɡorəf, a=Ru-Andrey Nikolaevich Kolmogorov.ogg, 25 April 1903 – 20 October 1987) was a Soviet ...
. It is also sometimes called the realizability interpretation, because of the connection with the
realizability theory of
Stephen Kleene
Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
. It is the standard explanation of intuitionistic logic.
The interpretation
The interpretation states what is intended to be a proof of a given
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
. This is specified by
induction on the structure of that formula:
*A proof of
is a pair
where
is a proof of
and
is a proof of
.
*A proof of
is either
where
is a proof of
or
where
is a proof of
.
*A proof of
is a construction (see ) that converts a (hypothetical) proof of
into a proof of
.
*A proof of
is a pair
where
is an element of
and
is a proof of
.
*A proof of
is a construction that converts an element
of
into a proof of
.
*The formula
is defined as
, so a proof of it is a construction that converts a proof of
into a proof of
.
*There is no proof of
, the
absurdity
Absurdity is the state or condition of being unreasonable, meaningless, or so unsound as to be irrational. "Absurd" is the adjective used to describe absurdity, e.g., "Tyler and the boys laughed at the absurd situation." It derives from the Lat ...
.
Note that it may be possible to prove
even though there are no proofs of
(or proofs of
);
is the hypothetical assertion that a proof of
could be built out of a proof of
, if one were available.
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
is the problem of reducing
to
; to solve it requires a method to solve problem
given a solution to problem
.
The interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of the formula
is a computation reducing the two terms to the same numeral.
Examples
The identity function is a proof of the formula
, no matter what ''P'' is.
The
law of non-contradiction expands to
:
* A proof of
is a construction that converts a proof of
into a proof of
.
* A proof of
is a pair of proofs
, where
is a proof of ''P'', and
is a proof of
.
* A proof of
is a construction that converts a proof of ''P'' into a proof of
.
Putting it all together, a proof of
is a construction that converts a pair
– where
is a proof of
, and
is a construction that converts a proof of
into a proof of
– into a proof of
.
There is a function
that does this, where
, proving the law of non-contradiction, no matter what ''P'' is.
Indeed, the same line of thought provides a proof for the ''
modus ponens
In propositional logic, (; MP), also known as (), implication elimination, or affirming the antecedent, is a deductive argument form and rule of inference. It can be summarized as "''P'' implies ''Q.'' ''P'' is true. Therefore, ''Q'' must ...
'' rule
as well, where
is any proposition.
On the other hand, the
law of excluded middle
In logic, the law of excluded middle or the principle of excluded middle states that for every proposition, either this proposition or its negation is true. It is one of the three laws of thought, along with the law of noncontradiction and t ...
expands to
, and in general has no proof. According to the interpretation, a proof of
is a pair
where ''a'' is 0 and ''b'' is a proof of
, or ''a'' is 1 and ''b'' is a proof of
. Thus if neither
nor
is provable then neither is
.
Definition of absurdity
It is not, in general, possible for a
logical system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in math ...
to have a formal negation operator such that there is a proof of "not"
exactly when there isn't a proof of
; see
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the phi ...
. The BHK interpretation instead takes "not"
to mean that
leads to absurdity, designated
, so that a proof of
is a construction converting a proof of
into a proof of absurdity.
A standard example of absurdity is found in dealing with arithmetic. Assume that 0 = 1, and proceed by
mathematical induction
Mathematical induction is a method for mathematical proof, proving that a statement P(n) is true for every natural number n, that is, that the infinitely many cases P(0), P(1), P(2), P(3), \dots all hold. This is done by first proving a ...
: 0 = 0 by the axiom of equality. Now (induction hypothesis), if 0 were equal to a certain
natural number
In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positive in ...
''n'', then 1 would be equal to ''n'' + 1, (
Peano axiom: S''m'' = S''n'' if and only if ''m'' = ''n''), but since 0 = 1, therefore 0 would also be equal to ''n'' + 1. By induction, 0 is equal to all numbers, and therefore any two natural numbers become equal.
Therefore, there is a way to go from a proof of 0 = 1 to a proof of any basic arithmetic equality, and thus to a proof of any complex arithmetic proposition. Furthermore, to get this result it was not necessary to invoke the Peano axiom that states that 0 is "not" the successor of any natural number. This makes 0 = 1 suitable as
in
Heyting arithmetic
In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.
Axiomatization
Heyting arithmetic can be characterized jus ...
(and the Peano axiom is rewritten 0 = S''n'' → 0 = S0). This use of 0 = 1 validates the
principle of explosion
In classical logic, intuitionistic logic, and similar logical systems, the principle of explosion is the law according to which any statement can be proven from a contradiction. That is, from a contradiction, any proposition (including its n ...
.
Definition of construction
The BHK interpretation will depend on the view taken about what constitutes a ''construction'' that converts one proof to another, or that converts an element of a domain to a proof. Different versions of
constructivism will diverge on this point.
Kleene's
realizability theory identifies constructions with the
computable function
Computable functions are the basic objects of study in computability theory. Informally, a function is ''computable'' if there is an algorithm that computes the value of the function for every value of its argument. Because of the lack of a precis ...
s. It deals with Heyting arithmetic, where the domain of quantification is the natural numbers and the primitive propositions are of the form ''x'' = ''y''. A proof of ''x'' = ''y'' is simply the trivial algorithm if ''x'' evaluates to the same number that ''y'' does (which is always decidable for natural numbers), otherwise there is no proof. These are then built up by induction into more complex algorithms.
If one takes
lambda calculus
In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
as defining the notion of a construction, then the BHK interpretation describes the
correspondence between natural deduction and lambda functions.
See also
*
Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-p ...
*
Logics for computability
Notes
References
*
*
External link
*
*
{{DEFAULTSORT:Brouwer-Heyting-Kolmogorov interpretation
Dependently typed programming
Functional programming
Constructivism (mathematics)