In short, there are two different logical principles, and ordinary mathematicians call both of them proof by contradiction. However, constructivist (aka intuitionist) mathematicians make a distinction between them: they "believe in" proof of negation, but not in proof by contradiction.

A lot of work has been done about formalizing mathematics in constructive logic. One big component of this is figuring out which uses of proof by contradiction are avoidable, and which one are essential (in the latter case the theorem statement has to be weakened for the constructive version). But this is all about proof by contradiction in the narrow sense. The usual proof about the irrationality of √2 is valid constructively.

¬¬ϕ ⇒ ϕ

The way I like to think of it is that, in constructive logic, both x and ¬¬x represent evidence for x—it's just that ¬¬x is weaker. You can still derive all the results you want, you simply have to be more explicit about whether you have constructive evidence or not.

I took formal systems in university some years ago and remember something about different axiom systems and how one school of thought rejected one particular rule of inference but was this the one?

I am trying to think of a world where this rule is not valid and not succeeding.

So, "2 + 2" is true because I can generate tangible evidence of it, but "the Collatz conjecture" is not true because I cannot. It's also not false. To be "false" I'd have to have tangible evidence of "the Collatz conjecture is false", a counterexample. This "I lack evidence" as neither truth nor falsehood is the characteristic of intuitionistic/constructive logic that makes it so interesting.

To be clear, there is now an element of time involved. Or, as others have stated, constructive logic reflects the "communicative nature" of proof. What I should have said a second ago is "The Collatz conjecture is not true (for me) (right now) (because I personally don't happen to have evidence for its validity yet)". If you had a (valid) proof it'd be true for you and once you communicated that proof to me it'd be true for me.

So in the case of rejecting "not not P => P", it's merely a statement of the fact that "not (not P)" failing to actually generate any evidence for "P", it merely shows that there isn't "not evidence". If you live in a world where things must be true or false (e.g., excluded middle holds) then this is sufficient, but if you demand I show you why "P" holds, then "not (not P)" is unsatisfactory.

¬¬¬¬ϕ ⇒ ¬¬ϕ

Expanding the definition of ¬, we must prove (((P⇒False)⇒False)⇒False)⇒P⇒False. I.e. we are given two assumptions

    f : ((P⇒False)⇒False)⇒False
    x : P

Indeed, this is a perfectly good function (so it's constructive). If we type that function into (say) a Haskell repl, the typechecker will infer an even more general type for it, but we can check that the type we wanted is an instance:

    ghci> :type (\f x -> f (\g -> g x)) 
    (\f x -> f (\g -> g x)) :: (((t2->t1)->t1)->t) -> t2 -> t
    gchi> type Not a = (a -> False)
    ghci> :type (\f x -> f (\g -> g x)) :: (Not (Not (Not p)))->Not p
    (\f x -> f (\g -> g x)) :: (Not (Not (Not p))) -> Not p

We can assume ¬p and we have to prove a contradiction. So we have to prove: ¬¬¬¬p, ¬p => _|_ Now, we know* that alpha => ¬¬alpha. So from ¬p, we can get ¬¬¬p. And from ¬(¬¬¬p) and (¬¬¬p) we arrive to _|_.

*To prove alpha => ¬¬alpha, we can assume ¬alpha and arrive at a contradiction, so we would have to rpove alpha, ¬alpha => _|_ and we are done.

In Natural Deduction:

    [¬p]1   [¬¬p]2
   ---------------
       _|_
   ----------2
      ¬¬¬p       ¬¬¬¬p
   -----------------------
           _|_
   -----------------------1
          ¬¬p

[1] http://en.wikipedia.org/wiki/Double-negation_translation

    proof : ¬¬¬¬ϕ ⇒ ¬¬ϕ
    proof (f : ((((a -> False) -> False) -> False) -> False)) =
      \ (z : a -> False) -> f (\afff -> afff (\aff -> aff z)))

Simplicity was the solution. The best theorems seem obvious in retrospect, because they are reduced into relationships between existing concepts.

I would recommend trying all angles of attack when searching for a proof. If it starts to take too long or you hit a dead end, try a different angle. Even if you discover a proof, try your other opening moves, look for a more elegant solution.

I believe Wolfram Alpha converges on this solution by performing some sort of weighted, breadth-first search on the permutations of an equation.

I highly recommend "Meta Math"[1] if you are interested in theories about entropy and algorithms that generate proofs.

[1] ("Meta Math", Gregory Chaitin, http://arxiv.org/pdf/math/0404335.pdf)

Oh, that's only a guideline for presenting your proves. Not for coming up with them in the first place. Mathematicians do exactly what you are suggesting already.

The first prove one finds is usually quite ugly, and then comes the simplification. Writers call it editing, programmers refactoring.

Suppose premises/axioms (B, C, ...) which don't depend on the value of A. Then, B=true AND C=true ... implies A=true by some logical argument, such as

A Or Not (B And C And ...) = True

In this case, the proof by contradiction is

Assume A=False But B=True, C=True, ... (Since they dont depend on A) Apply above constructive argument So A is true, A CONTRADICTION

Proofs by contradiction can often be of this type so the first and last lines can be removed.

The question is, what other types can there be?

-- John Barrow

I almost always start with contradiction as my initial method of choice when taking exams because you don't always have time to completely rewrite your proofs. Contradiction helps with this since it naturally encompasses proving by contrapositive also. Because if you're trying to prove that p->q, you can assume p and ~q and getting to ~p is a contradiction since p^~p (and this is the same structure as a proof by contrapositive if you got to this line without assuming p). And of course if you find any other absurdities along the way sooner, you're done quicker.

This is nice because a proof by contrapositive is more or less equivalent to a direct proof. So simply by always starting with proof by contradiction, you cover the cases where the theorem:

- is simple enough for you to find out exactly why it's true (direct proof hidden in the contrapositive).

- is complex and wide reaching enough for you to hit an absurdity quickly

Where is that conclusion drawn? This is an blog post for research (and armchair) mathematicians, not students trying to sit an exam.

>In which case, perhaps the advice that I give to students — proof by contradiction is a very useful tool, but try not to use it unless you really need it — is, though not completely precise, about the best one can do.

:-)

In that way, it avoids issues with deducing things from a set of pre-prescribed beliefs. In fact, it fights against them.

The same way that induction is the extension of syllogism into countable sets?

But what if Not X leads to a contradiction and we can't seem to find a contradiction when we assume X, but we aren't sure there isn't one? Have we proven X by contradiction, or is it really a paradox and there is some nonsensical operation somewhere?

I remember wondering something likethat before.

All rational numbers have the property that their square is not 2. (Should be a simple proof by induction on the denominator.) The square root of two does not have that property, and is therefore not rational.

Is the contradiction hiding in my implied definition, my implied induction proof, somewhere else?

    All rational numbers have the property that their square is not 2

   2 not in {r^2 for r in rationals}

   sqrt(2) not in {r for r in rationals}

   sqrt(2) not in rationals

Assume n,m,x integer, and n^2/m^2=x. I claim x!=2. Proof: Write out both n and m's prime factorizations. Their squares' prime factorizations each contain an even number of all primes (zero is even). Therefore, for every prime, x's prime factorization contains an even number of it as well. Therefore x is not 2.

Your proof hinges on the not-directly-stated words "so, if x were 2, we would reach an impossibility" where impossibility == contradiction.

They may be equivalent, but not if we count proof by contradiction as special.

In response to edit: No, it doesn't. Having proven that x contains an even number of 2s as factors, it follows that x is not two. 2 does not have an even number of 2s as factors, x does, therefore they are different. No contradiction required.

The key point here is that you are partitioning the possibilities in a binary fashion: either x has even number of prime factors or it does not. You've shown that it must not have an even number of prime factors. You haven't shown that it isn't 2. You implied that if it were true, that would contradict what you have shown.

How you go from "X has an even number of prime factors" to "X can't be 2" is important.

You're right that they are "essentially" the same proof, but excluding contradictions is weird, a bit like excluding the letter e. Rephrasing a proof to not use it may be possible in some cases.

This is where you are implicitly employing proof by contradiction. Why do you take two cases and not three? Or four? What assumption allows you to restrict your conclusions like that?

Probably the Law of the Excluded Middle: (P or ~P). (This is equivalent to ~~p = p.)

Once you assume or derive either of those, you have validated proof by contradiction.

Let's imagine I had shown that something was either one or two. You seem to be claiming I could not take positive proofs assuming each of them and turn it into a full proof.

When you break it down to the logical axioms, you can't use cases like that. Try it yourself. You get something like this:

Let A: (k > 0)

B: (k = 0)

k is a whole number, therefore A v B.

A -> X !=2

B -> X !=2

Okay, from here, you need to deduce X != 2. Traditionally we do this by applying proof by cases, but as I showed in my other comment, this requires the law of the excluded middle.

I don't see any other propositional logic axioms we can apply to achieve the same result.

I think that's because you don't know A v B. But in my case you can directly prove A v B.

The form is (A v B, A -> C, B -> C) -> C.

https://en.wikipedia.org/wiki/Proof_by_exhaustion says that this is called a direct proof.

Here is a more rigorous form of what you've said there:

    Let X be an integer with a prime factorization in the form 2^(2k) * p_1 * p_2 ... * p_n where k is a positive integer and p_i for any i is a prime not equal to 2.

    Proposition: X is not 2

    Proof:

    Assume X is 2.

    The prime factorization of X is:

    X = 2

    By the definition of X, we have:

    2 = 2^(2k) * p_1 * p_2 ... * p_n

    Since we defined k to be a positive integer, we have

    min(2^(2k)) = 2^(2(min(k)) = 2^(2*1) = 4

    So we have:

    2^(2k) >= 4

    So we have:

    2^(2k) > 2

    Since p_i for all i are all positive integers, we have:

    2 < 2^(2k) * p_1 * p_2 ... * p_n

    So we have:

    2 != 2^(2k) * p_1 * p_2 ... * p_n

    Thus:

    2 != X

    And we have arrived at a contradiction.

Consider k. Either it is 0, or greater. Consider 0. In that case, X is not divisible by 2, hence cannot be 2.

Now consider k positive. (My original proof didn't show k wa positive, so I needed to deal seperately.)

Use your proof to show that 2^(2k) > 2, and then 2!=X. As far as I can tell you never actually used the assumption that 2=x, so that can be deleted from the proof and it remains valid.

The briefest amount of work in mathematical deduction or symbolic logic will cause you to raise an eyebrow whenever anyone insists "you can't prove a negative."

Every negative statement has a positive formulation buried within it. Or, no negative statement exists that lacks a positive formulation, and vice versa.

As stated, p = q = 0 is a valid solution.