ImperialViolet

• Understanding The Linux Virtual Memory Manager. Also see the code commentary

Ok, after talking with one of the maths people here about this, it boils down to this: proof by contractions works only if you accept A∨¬A. That's called the law of the excluded middle.

Now, if you look that up (e.g. on MathWorld) you'll find at it says something like "this means that A is either true or false". But it doesn't. A∨¬A means that either A or ¬A is a theorm (i.e. can be reached on our axiom tree). So it really says either A or ¬A is provable; but Gödel has shown otherwise.

And in my logic notes the following proof of A∨¬A was given:

1 ¬(A∨¬A) assume 2 A assume 3 A∨¬A ∨I(2) 4 ⊥ ¬E(1,3) 5 ¬A ¬I(2,4) 6 A∨¬A ∨I(5) 7 ⊥ ¬E(1,6)
8	¬¬(A∨¬A)	¬I(1,7)
9	A∨¬A	¬¬(8)

(Box proofs are a pain to typeset in HTML)

That means that the basis of proof by contradiction is proven using proof by contradiction. (it also has a ¬¬ elimination, but that's not the subject of this post)

Thankfully, a google shows that I'm not the only person to ever think this way. (Which makes me a little more confident that someone like Ralph or Bram isn't going to stomp me with a devistating counter argument). Intuitionistic Logic seems be (at least) a similar school of thought. A few more links that I haven't fully digested yet:

• K5: Alternative Logics
• The Law of the Excluded Middle
• The Continuum Hypothesis