see how, consider the statement H(M) stating "Turing machine M halts or does not halt". Its negation ¬H(M) states that "M neither halts nor does not halt", which is false by the law of noncontradiction (which is intuitionistically valid). If proof by contradiction were intuitionistically valid, we would obtain an algorithm for deciding whether an arbitrary Turing machine M halts, thereby violating the (intuitionistically valid) proof of non-solvability of the Halting problem. A proposition P which satisfies is known as a ¬¬-stable proposition. Thus in intuitionistic logic proof by contradiction is not universally valid, but can only be applied to the ¬¬-stable propositions. An instance of such a proposition is a decidable one, i.e., satisfying . Indeed, the above proof that the law of excluded middle implies proof by contradiction can be repurposed to show that a decidable proposition is ¬¬-stable. A typical example of a decidable proposition is a statement that can be checked by direct computation, such as " is prime" or " divides ". Examples of proofs by contradiction Euclid's Elements An early occurrence of proof by contradiction can be found in Euclid's Elements, Book 1, Proposition 6: If in a triangle two angles equal one another, then the sides opposite the equal angles also equal one another. The proof proceeds by assuming that the opposite angles are not equal, and derives a contradiction. Hilbert's Nullstellensatz An influential proof by contradiction was given by David Hilbert. His Nullstellensatz states: If are polynomials in indeterminates with complex coefficients, which have no common complex zeros, then there are polynomials such that Hilbert proved the statement by assuming that there are no such polynomials and derived a contradiction. Infinitude of primes Euclid's theorem states that there are infinitely many primes. In Euclid's Elements the theorem is stated in Book IX, Proposition 20: Prime numbers are more than any assigned multitude of prime numbers. Depending on how we formally write the above statement, the usual proof takes either the form of a proof by contradiction or a refutation by contradiction. We present here the former, see below how the proof is done as refutation by contradiction. If we formally express Euclid's theorem as saying that for every natural number there is a prime bigger than it, then we employ proof by contradiction, as follows. Given any number , we seek to prove that there is a prime larger than . Suppose