### More on Proof by Contradiction (22 Jan 2003)

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:

| ||||||||||||||||||||||||||

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: