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 . Definition of 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. Definition of 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