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



Proof by contradiction in a topos
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](http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/) 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. 


