HOME

TheInfoList



OR:

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 P \wedge Q is a pair \langle a, b \rangle where a is a proof of P and b is a proof of Q. *A proof of P \vee Q is either \langle 0, a \rangle where a is a proof of P or \langle 1, b\rangle where b is a proof of Q. *A proof of P \to Q is a construction (see ) that converts a (hypothetical) proof of P into a proof of Q. *A proof of (\exists x S) (Px) is a pair \langle x, a \rangle where x is an element of S and a is a proof of Px. *A proof of (\forall x S) (Px) is a construction that converts an element x of S into a proof of Px. *The formula \neg P is defined as P \to \bot, so a proof of it is a construction that converts a proof of P into a proof of \bot. *There is no proof of \bot, 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 P \to Q even though there are no proofs of P (or proofs of Q); P \to Q is the hypothetical assertion that a proof of Q could be built out of a proof of P, 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 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 interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of the formula x = y is a computation reducing the two terms to the same numeral.


Examples

The identity function is a proof of the formula P \to P, no matter what ''P'' is. The law of non-contradiction \neg (P \wedge \neg P) expands to (P \wedge (P \to \bot)) \to \bot: * A proof of (P \wedge (P \to \bot)) \to \bot is a construction that converts a proof of (P \wedge (P \to \bot)) into a proof of \bot. * A proof of (P \wedge (P \to \bot)) is a pair of proofs \langle a, b \rangle, where a is a proof of ''P'', and b is a proof of P \to \bot. * A proof of P \to \bot is a construction that converts a proof of ''P'' into a proof of \bot. Putting it all together, a proof of (P \wedge (P \to \bot)) \to \bot is a construction that converts a pair \langle a, b \rangle – where a is a proof of P, and b is a construction that converts a proof of P into a proof of \bot – into a proof of \bot. There is a function f that does this, where f(\langle a, b \rangle) = b(a), 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 (P \wedge (P \to Q)) \to Q as well, where Q 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 ...
P \vee (\neg P) expands to P \vee (P \to \bot), and in general has no proof. According to the interpretation, a proof of P \vee (\neg P) is a pair \langle a, b \rangle where ''a'' is 0 and ''b'' is a proof of P, or ''a'' is 1 and ''b'' is a proof of P \to \bot. Thus if neither P nor P \to \bot is provable then neither is P \vee (\neg P).


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" P exactly when there isn't a proof of P; 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" P to mean that P leads to absurdity, designated \bot, so that a proof of \lnot P is a construction converting a proof of P 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 \bot 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)