Brouwer-Heyting-Kolmogorow interpretation

The Brouwer-Heyting-Kolmogorow interpretation , or BHK interpretation for short , is an interpretation of the intuitionistic logic in mathematical logic that was proposed by LEJ Brouwer and Arend Heyting and, independently of them, by Andrei Kolmogorow . Because of its connection to the proof-theoretical feasibility according to Stephen Kleene , it is also referred to as the feasibility interpretation .

The interpretation

According to the BHK interpretation refers to the proof of a logical formula. It is indicated by induction on the structure.

• A proof of is a pair , where is a proof of and a proof of . ${\displaystyle \varphi \wedge \psi }$ ${\displaystyle (a,b)}$ ${\displaystyle a}$ ${\displaystyle \varphi }$ ${\displaystyle b}$ ${\displaystyle \psi }$
• A proof of is a pair where is equal and a proof of , or is and a proof of . ${\displaystyle \varphi \vee \psi }$ ${\displaystyle (i,a)}$ ${\displaystyle i}$ ${\displaystyle 0}$ ${\displaystyle a}$ ${\displaystyle \varphi }$ ${\displaystyle i}$ ${\displaystyle 1}$ ${\displaystyle a}$ ${\displaystyle \psi }$
• A proof of is a function that converts proofs from to proofs from . ${\displaystyle \varphi \to \psi }$ ${\displaystyle f}$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$
• A proof of is a pair , where is an element of , and a proof of . ${\displaystyle \exists x\in S:\varphi (x)}$ ${\displaystyle (t,a)}$ ${\displaystyle t}$ ${\displaystyle S}$ ${\displaystyle a}$ ${\displaystyle \varphi (t)}$
• A proof of is a function that converts elements of into a proof of . ${\displaystyle \forall x\in S:\varphi (x)}$ ${\displaystyle f}$ ${\displaystyle t}$ ${\displaystyle S}$ ${\displaystyle \varphi (t)}$
• The formula is not a formula in the strict sense and is understood as an abbreviation for , so it has a function as proof that converts proofs of into proofs of . ${\displaystyle \neg \varphi }$ ${\displaystyle \varphi \to \bot }$ ${\displaystyle f}$ ${\displaystyle \varphi }$ ${\displaystyle \bot }$
• There is no evidence of the absurdity represented by . ${\displaystyle \bot }$

The interpretation of an atomic proposition is assumed to be given by the context. In the context of arithmetic, a proof of the formula is a calculation that reduces the two terms and to the same number. ${\displaystyle s=t}$ ${\displaystyle s}$ ${\displaystyle t}$

Kolmogorov followed the same path, but formulated it using the terms problem and solution . Thus, confirming the validity of a formula is claiming to know a solution to the problem that the formula represents. For example, the problem is to cut down on ; a solution needs a method of solving the problem , if there is a solution for . ${\displaystyle \varphi \to \psi }$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle \psi }$ ${\displaystyle \varphi }$

Examples

The identity is a proof of the formula , regardless of which specific formula is. ${\displaystyle \varphi \to \varphi }$ ${\displaystyle \varphi }$

The law of noncontradiction becomes : ${\displaystyle \neg (\varphi \wedge \neg \varphi )}$ ${\displaystyle (\varphi \wedge (\varphi \to \bot ))\to \bot }$

• A proof of is a function that converts a proof of into a proof of . ${\displaystyle (\varphi \wedge (\varphi \to \bot ))\to \bot }$ ${\displaystyle f}$ ${\displaystyle (\varphi \wedge (\varphi \to \bot ))}$ ${\displaystyle \bot }$
• A proof of is a pair of proofs , where a proof of and is a proof of . ${\displaystyle (\varphi \wedge (\varphi \to \bot ))}$ ${\displaystyle (a,b)}$ ${\displaystyle a}$ ${\displaystyle \varphi }$ ${\displaystyle b}$ ${\displaystyle \varphi \to \bot }$
• A proof of is a function that converts a proof of into a proof of . ${\displaystyle \varphi \to \bot }$ ${\displaystyle g}$ ${\displaystyle \varphi }$ ${\displaystyle \bot }$

The function fits the task and proves the law of noncontradiction, regardless of which formula is. ${\displaystyle f(a,g)=g(a)}$ ${\displaystyle \varphi }$

The same approach gives a proof of the modus ponens , where is any formula. ${\displaystyle (\varphi \wedge (\varphi \to \psi ))\to \psi }$ ${\displaystyle \psi }$

On the other hand, the principle of the excluded third party , specifically , generally, has no proof. According to the interpretation, a proof of is a pair where equal and a proof of is, or is and a proof of . If neither nor is provable, it also fails . Concrete formulas for which the principle of excluded third parties applies, e.g. B. because they can be derived, are called decidable . Likewise , so , generally has no evidence. Formulas for which the implication applies are called stable . ${\displaystyle \varphi \vee (\neg \varphi )}$ ${\displaystyle \varphi \vee (\varphi \to \bot )}$ ${\displaystyle \varphi \vee \neg \varphi }$ ${\displaystyle (i,a)}$ ${\displaystyle i}$ ${\displaystyle 0}$ ${\displaystyle a}$ ${\displaystyle \varphi }$ ${\displaystyle i}$ ${\displaystyle 1}$ ${\displaystyle a}$ ${\displaystyle \neg \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \varphi \to \bot }$ ${\displaystyle \varphi \vee \neg \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \lnot \lnot \varphi \to \varphi }$ ${\displaystyle ((\varphi \to \bot )\to \bot )\to \varphi }$ ${\displaystyle \varphi }$

What is absurdity?

According to Gödel's incompleteness theorem , a formal system can not have a formal negation , so that there is a proof of if and only if there is no proof of . The BHK interpretation interprets in such a way that leads to absurdity that is written as. A proof of is a function that converts a proof of into a proof of an absurdity. ${\displaystyle \neg }$ ${\displaystyle \neg \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \neg \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \bot }$ ${\displaystyle \neg \varphi }$ ${\displaystyle \varphi }$

A standard example of absurdity in arithmetic is formula . By means of complete induction , it follows that all natural numbers are equal. ${\displaystyle 0=1}$

Hence there is a way to get from to a proof of every basic arithmetic equality, and thus to a proof of any complex statement. This result also does not need the axiom of Peano arithmetic that it is not the successor of any natural number. This makes a suitable and common candidate for in Heyting arithmetic . The Peano axiom thus becomes . With the system fulfills the principle of Ex falso quodlibet . ${\displaystyle 0=1}$ ${\displaystyle 0}$ ${\displaystyle 0=1}$ ${\displaystyle \bot }$ ${\displaystyle 0=n+1\to 0=1}$ ${\displaystyle 0=1}$

What is a function?

The BHK interpretation depends heavily on the view of what counts as a function or should be permitted. In constructivism different views are represented.

Kleene's theory of feasibility only allows for the computable functions. It uses Heyting arithmetic, where the quantified range consists of the natural numbers. Basic formulas have the form . One proof consists of the algorithm that evaluates both sides and returns whether it was the same number. Otherwise there is no proof. More complex algorithms then build on this. ${\displaystyle x=y}$

If one takes the lambda calculus as the basis of functions, the BHK interpretation says nothing other than the correspondence between natural reasoning and functions.

credentials

• Anne Troelstra : History of Constructivism in the Twentieth Century . 1991 (English, [1] [PDF; 4.0 MB ]).
• Anne Troelstra : Constructivism and Proof Theory (draft) . 2003 ( [2] [PDF; 286 kB ]).