# ImperialViolet

### 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:

1¬(A∨¬A)assume
 2 A assume 3 A∨¬A ∨I(2) 4 ⊥ ¬E(1,3)
5¬A¬I(2,4)
6A∨¬A∨I(5)
7¬E(1,6)
8¬¬(A∨¬A)¬I(1,7)
9A∨¬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: