To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
Languages
Recent
Show all languages
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds

Brouwer–Heyting–Kolmogorov interpretation

From Wikipedia, the free encyclopedia

In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and 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

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:

  • A proof of is a pair <a, b> where a is a proof of and b is a proof of .
  • A proof of is a pair <a, b> where a is 0 and b is a proof of , or a is 1 and b is a proof of .
  • A proof of is a function that converts a proof of into a proof of .
  • A proof of is a pair <a, b> where a is an element of S, and b is a proof of .
  • A proof of is a function that converts an element a of S into a proof of .
  • The formula is defined as , so a proof of it is a function f that converts a proof of into a proof of .
  • There is no proof of (the absurdity, or bottom type (nontermination in some programming languages)).

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 is the problem of reducing Q to P; to solve it requires a method to solve problem Q given a solution to problem P.

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 function that converts a proof of into a proof of .
  • A proof of is a pair of proofs <a, b>, where is a proof of P, and is a proof of .
  • A proof of is a function that converts a proof of P into a proof of .

Putting it all together, a proof of is a function that converts a pair <a, b> – where is a proof of P, and is a function that converts a proof of P 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 as well, where is any proposition.

On the other hand, the law of excluded middle expands to , and in general has no proof. According to the interpretation, a proof of is a pair <a, b> where a is 0 and b is a proof of P, or a is 1 and b is a proof of . Thus if neither P nor is provable then neither is .

What is absurdity?

It is not, in general, possible for a logical system 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. The BHK interpretation instead takes "not" to mean that leads to absurdity, designated , so that a proof of is a function 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: 0 = 0 by the axiom of equality. Now (induction hypothesis), if 0 were equal to a certain natural number n, then 1 would be equal to n + 1, (Peano axiom: Sm = Sn 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 (and the Peano axiom is rewritten 0 = Sn → 0 = S0). This use of 0 = 1 validates the principle of explosion.

What is a function?

The BHK interpretation will depend on the view taken about what constitutes a function 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 the functions with the computable functions. 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 as defining the notion of a function, then the BHK interpretation describes the correspondence between natural deduction and functions.

References

  • Troelstra, A. (1991). "History of Constructivism in the Twentieth Century" (PDF). Cite journal requires |journal= (help)
  • Troelstra, A. (2003). "Constructivism and Proof Theory (draft)". CiteSeerX 10.1.1.10.6972. Cite journal requires |journal= (help)
This page was last edited on 26 January 2021, at 22:37
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.