MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
up vote 10 down vote accepted

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.

share|cite|improve this answer
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


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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.