# Proof by contradiction in a topos

In a topos which is not Boolean topos, can we use proof by contradiction?

-

It depends on what examples you have in mind when you say "proof by contradiction". This topic has come up a number of times recently at MO, but I recommend to your attention the useful blog post by Andrej Bauer, which explains that there is a subtle distinction to be made between "proof of negation" and "proof by contradiction".

If the proposition to be proved is already of the form $\neg p$, then it may help to recall that $\neg p$ is (by definition) the weakest assumption one could make such its conjunction with $p$ entails falsity (in symbols, $x \leq \neg p$ iff $x \wedge p \leq 0$). This is true in intuitionistic logic as well as in classical logic. So a proof of a negated proposition $\neg p$ would quite properly begin, "suppose $p$, then ... contradiction". Many people call this a proof by contradiction, because the structure of the argument-phrasing looks just like any old proof by contradiction.

An example of this is Cantor's theorem (that there is no surjection from a set to its power set, or $\neg$ "there exists a surjection..."). This can be formulated in any topos and is true in any topos, Boolean or not.

(If this helps, notice that in intuitionistic logic, we have that $\neg p$ is equivalent to $\neg \neg \neg p$: a negated proposition is always equivalent to its double negation.)

But contrast this with for example the Hahn-Banach theorem: every locally convex topological vector space admits a continuous functional to the ground field. This proposition, which is not in negated form, is a prime example of something which has no constructive proof. A typical method of proof would be something like "by Zorn's lemma, there is a maximal closed subspace that admits such a continuous functional, and suppose this were not the whole space" and eventually derive a contradiction. This type of reasoning is not valid in a general topos.

For another example, consider "$\sqrt{2}$ is irrational". This is a negative proposition: "$\neg (\exists p, q \in \mathbb{Z}_+ \; p^2 = 2 q^2)$". The usual arithmetic proofs are valid in any topos.

-
Yes, that's a good answer. The word topos is a distraction. One should just learn how to write proofs constructively wherever possible. Maybe the result that alphaa wants can be proved intuitionistically. – Paul Taylor May 2 '13 at 18:55

No.

There is no need to say any more than that, since the answer is in the question, except that MathOverflow will not let me submit something with so few characters.

-