Topological skeleton

2014-01-03T06:55:25Z

24.6.47.6: /* Skeletonization algorithms */

In [[mathematical logic]], the '''Brouwer–Heyting–Kolmogorov interpretation''', or '''BHK interpretation''', of [[intuitionistic logic]] was proposed by [[L. E. J. Brouwer]], [[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 exactly what is intended to be a proof of a given [[Formula (mathematical logic)|formula]]. This is specified by [[induction on the structure]] of that formula:

*A proof of <math>P \wedge Q</math> is a pair <''a'', ''b''> where ''a'' is a proof of ''P'' and ''b'' is a proof of ''Q''.
*A proof of <math>P \vee Q</math> 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 ''Q''.
*A proof of <math>P \to Q</math> is a function ''f'' which converts a proof of ''P'' into a proof of ''Q''.
*A proof of <math>\exists x \in S : \phi(x)</math> is a pair <''a'', ''b''> where ''a'' is an element of ''S'', and ''b'' is a proof of ''φ(a)''.
*A proof of <math>\forall x \in S : \phi(x)</math> is a function ''f'' which converts an element ''a'' of ''S'' into a proof of ''φ(a)''.
*The formula <math>\neg P</math> is defined as <math>P \to \bot</math>, so a proof of it is a function ''f'' which converts a proof of ''P'' into a proof of <math>\bot</math>.
*There is no proof of <math>\bot</math> (the absurdity).

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 <math>P \to Q</math> 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 <math>P \to P</math>, no matter what P is.

The [[law of non-contradiction]] <math>\neg (P \wedge \neg P)</math> expands to <math>(P \wedge (P \to \bot)) \to \bot</math>:
* A proof of <math>(P \wedge (P \to \bot)) \to \bot</math> is a function ''f'' which converts a proof of <math>(P \wedge (P \to \bot))</math> into a proof of <math>\bot</math>.
* A proof of <math>(P \wedge (P \to \bot))</math> is a pair of proofs <''a'',''b''>, where ''a'' is a proof of ''P'', and ''b'' is a proof of <math>P \to \bot</math>.
* A proof of <math>P \to \bot</math> is a function which converts a proof of ''P'' into a proof of <math>\bot</math>.
Putting it all together, a proof of <math>(P \wedge (P \to \bot)) \to \bot</math> is a function ''f'' which converts a pair <''a'',''b''> – where ''a'' is a proof of ''P'', and ''b'' is a function which converts a proof of ''P'' into a proof of <math>\bot</math> – into a proof of <math>\bot</math>.
The function <math>f(\langle a, b \rangle) = b(a)</math> fits the bill, proving the law of non-contradiction, no matter what P is.

On the other hand, the [[law of excluded middle]] <math>P \vee (\neg P)</math> expands to <math>P \vee (P \to \bot)</math>, and in general has no proof. According to the interpretation, a proof of <math>P \vee (\neg P)</math> 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 <math>P \to \bot</math>. Thus if neither ''P'' nor <math>P \to \bot</math> is provable then neither is <math>P \vee (\neg P)</math>.

== 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" P'' exactly when there isn't a proof of ''P'' ; see [[Gödel's incompleteness theorems]]. The BHK interpretation instead takes ''"not" P'' to mean that ''P'' leads to absurdity, designated <math>\bot</math>, so that a proof of ''¬P'' is a function 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]]: 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 arithmetic|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 which states that 0 is "not" the successor of any natural number. This makes 0=1 suitable as <math>\bot</math> in Heyting arithmetic (and the Peano axiom is rewritten 0 = '''S'''''n'' → 0 = '''S'''0). 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'' which converts one proof to another, or which converts an element of a domain to a proof. Different versions of [[constructivism (mathematics)|constructivism]] will diverge on this point.

Kleene's realizability theory identifies the functions with the [[computable function]]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]] as defining the notion of a function, then the BHK interpretation describes the [[Curry–Howard correspondence|correspondence]] between natural deduction and functions.

== References ==
*{{cite paper |authorlink=A. S. Troelstra |last=Troelstra |first=A. |title=History of Constructivism in the Twentieth Century |year=1991 |url=http://staff.science.uva.nl/~anne/hhhist.pdf |doi= }}
*{{cite paper |last=Troelstra |first=A. |title=Constructivism and Proof Theory |year=2003 |url=http://staff.science.uva.nl/~anne/eolss.pdf |doi= }}

{{DEFAULTSORT:Brouwer-Heyting-Kolmogorov interpretation}}
[[Category:Dependently typed programming]]
[[Category:Functional programming]]
[[Category:Constructivism (mathematics)]]

formulasearchengine - User contributions [en]

Topological skeleton