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 . It is the standard explanation of intuitionistic logic.
17-424: BHK is a three-letter abbreviation that may refer to: BHK interpretation of intuitionistic predicate logic Baby hamster kidney cells used in molecular biology Bachelor of Human Kinetics (BHk) degree. Baltische Historische Kommission , organization dealing with history of Baltic Germans Biblia Hebraica (Kittel) , by Rudolf Kittel British Hong Kong ,
34-404: A ) {\displaystyle 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 rule ( P ∧ ( P → Q ) ) → Q {\displaystyle (P\wedge (P\to Q))\to Q} as well, where Q {\displaystyle Q}
51-447: A certain natural number 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
68-581: A former colony in the Qing Dynasty and later in the People's Republic of China , now Hong Kong Bush Hill Park railway station , London, UK, National Rail station code Bukhara International Airport , Uzbekistan, IATA code Prosperous Armenia , Armenian political party Bedroom - Hall - Kitchen , as used in India to describe apartments: 2 BHK, 3 BHK… — see Wiktionary:BHK Topics referred to by
85-418: A proof of ¬ P {\displaystyle \lnot P} is a function converting a proof of P {\displaystyle 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 : 0 = 0 by the axiom of equality. Now (induction hypothesis), if 0 were equal to
102-437: A proof of ( P ∧ ( P → ⊥ ) ) → ⊥ {\displaystyle (P\wedge (P\to \bot ))\to \bot } is a function f {\displaystyle f} that converts a pair < a , b > – where a {\displaystyle a} is a proof of P {\displaystyle P} , and b {\displaystyle b}
119-543: 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 ⊥ {\displaystyle \bot } in Heyting arithmetic (and the Peano axiom is rewritten 0 = S n → 0 = S 0). This use of 0 = 1 validates
136-402: Is a function that converts a proof of P {\displaystyle P} into a proof of ⊥ {\displaystyle \bot } – into a proof of ⊥ {\displaystyle \bot } . There is a function f {\displaystyle f} that does this, where f ( ⟨ a , b ⟩ ) = b (
153-429: 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 P → ⊥ {\displaystyle P\to \bot } . Thus if neither P nor P → ⊥ {\displaystyle P\to \bot } is provable then neither is P ∨ ( ¬ P ) {\displaystyle P\vee (\neg P)} . It
170-464: Is any proposition. On the other hand, the law of excluded middle P ∨ ( ¬ P ) {\displaystyle P\vee (\neg P)} expands to P ∨ ( P → ⊥ ) {\displaystyle P\vee (P\to \bot )} , and in general has no proof. According to the interpretation, a proof of P ∨ ( ¬ P ) {\displaystyle P\vee (\neg P)}
187-402: Is different from Wikidata All article disambiguation pages All disambiguation pages BHK 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: The interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of
SECTION 10
#1732781074812204-536: Is not, in general, possible for a logical system to have a formal negation operator such that there is a proof of "not" P {\displaystyle P} exactly when there isn't a proof of P {\displaystyle P} ; see Gödel's incompleteness theorems . The BHK interpretation instead takes "not" P {\displaystyle P} to mean that P {\displaystyle P} leads to absurdity, designated ⊥ {\displaystyle \bot } , so that
221-791: Is the problem of reducing Q {\displaystyle Q} to P {\displaystyle P} ; to solve it requires a method to solve problem Q {\displaystyle Q} given a solution to problem P {\displaystyle P} . The identity function is a proof of the formula P → P {\displaystyle P\to P} , no matter what P is. The law of non-contradiction ¬ ( P ∧ ¬ P ) {\displaystyle \neg (P\wedge \neg P)} expands to ( P ∧ ( P → ⊥ ) ) → ⊥ {\displaystyle (P\wedge (P\to \bot ))\to \bot } : Putting it all together,
238-407: The principle of explosion . 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
255-402: 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
272-403: The formula x = y {\displaystyle x=y} 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 P → Q {\displaystyle P\to Q}
289-403: The same term [REDACTED] This disambiguation page lists articles associated with the title BHK . If an internal link led you here, you may wish to change the link to point directly to the intended article. Retrieved from " https://en.wikipedia.org/w/index.php?title=BHK&oldid=1155436788 " Category : Disambiguation pages Hidden categories: Short description
#811188