5 ms·

See also Andrej Bauer's "reply article", Proof of Negation and Proof by Contradiction: http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradi

See also Andrej Bauer's "reply article", Proof of Negation and Proof by Contradiction: http://math.andrej.com/2010/03/29/proof-of-negation-and-proof-by-contradiction/ http://math.andrej.com/2010/03/29/proof-of-negation-and-proo... 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.

monochromatic 12y ago
The "problem" is basically that constructivists don't believe that this is a valid inference: ¬¬ϕ ⇒ ϕ
- iamcurious 12y ago
  And even that is less of a problem if you take into account that they still accept: ¬¬¬¬ϕ ⇒ ¬¬ϕ
  - monochromatic 12y ago
    Do they really? Why?
    - tel 12y ago
      proof : ¬¬¬¬ϕ ⇒ ¬¬ϕ proof (f : ((((a -> False) -> False) -> False) -> False)) = \ (z : a -> False) -> f (\afff -> afff (\aff -> aff z)))
    - iamcurious 12y ago
      It just follows from the axioms. They accept that a proof of ¬ p can be a proof that takes p and arrives to a contradiction. And that a contradiction is a formula and its negation. From that we can prove ¬¬¬¬p => ¬¬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 This has been generalized to translate classical theorems into constructive theorems.[1] Just like this case, though, the resulting theorems are full of double negations. [1] http://en.wikipedia.org/wiki/Double-negation_translation http://en.wikipedia.org/wiki/Double-negation_translation
    - vilhelm_s 12y ago
      It may be slightly easier to work through it for the formula ¬¬¬P ⇒ ¬P. (This also a constructive tautology, and the above formula is an instance of it, taking P = ¬ϕ). So let's prove that. 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 and should prove False. So we can use the assumption f, provided we can find an argument of type ((P⇒False)⇒False) to call it with. And in fact that's easy: (λg. g x). The full proof term is λf.λx. f (λg. g x) 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
- tikhonj 12y ago
  The really fascinating thing is that the distinction between ¬¬x and x actually parallels the distinction between proof by contradiction and normal proofs. That is, if you have any classical proof of x, you have a constructive proof of ¬¬x. 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.
- sireat 12y ago
  What is the justification for not believing that from a double negation of A follows A is a valid inference? 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.
  - tel 12y ago
    The simplest intuition is to exchange "truth" as the airy concept of "is valid/reflects the world" with "I possess tangible evidence to the case". 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.
  - tunesmith 12y ago
    One example is to define truth as provability. If A isn't unprovable, it doesn't mean that A is provable.

monochromatic 12y ago

The "problem" is basically that constructivists don't believe that this is a valid inference: ¬¬ϕ ⇒ ϕ

iamcurious 12y ago
And even that is less of a problem if you take into account that they still accept: ¬¬¬¬ϕ ⇒ ¬¬ϕ
- monochromatic 12y ago
  Do they really? Why?
  - tel 12y ago
    proof : ¬¬¬¬ϕ ⇒ ¬¬ϕ proof (f : ((((a -> False) -> False) -> False) -> False)) = \ (z : a -> False) -> f (\afff -> afff (\aff -> aff z)))
  - iamcurious 12y ago
    It just follows from the axioms. They accept that a proof of ¬ p can be a proof that takes p and arrives to a contradiction. And that a contradiction is a formula and its negation. From that we can prove ¬¬¬¬p => ¬¬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 This has been generalized to translate classical theorems into constructive theorems.[1] Just like this case, though, the resulting theorems are full of double negations. [1] http://en.wikipedia.org/wiki/Double-negation_translation http://en.wikipedia.org/wiki/Double-negation_translation
  - vilhelm_s 12y ago
    It may be slightly easier to work through it for the formula ¬¬¬P ⇒ ¬P. (This also a constructive tautology, and the above formula is an instance of it, taking P = ¬ϕ). So let's prove that. 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 and should prove False. So we can use the assumption f, provided we can find an argument of type ((P⇒False)⇒False) to call it with. And in fact that's easy: (λg. g x). The full proof term is λf.λx. f (λg. g x) 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
tikhonj 12y ago
The really fascinating thing is that the distinction between ¬¬x and x actually parallels the distinction between proof by contradiction and normal proofs. That is, if you have any classical proof of x, you have a constructive proof of ¬¬x. 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.
sireat 12y ago
What is the justification for not believing that from a double negation of A follows A is a valid inference? 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.
- tel 12y ago
  The simplest intuition is to exchange "truth" as the airy concept of "is valid/reflects the world" with "I possess tangible evidence to the case". 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.
- tunesmith 12y ago
  One example is to define truth as provability. If A isn't unprovable, it doesn't mean that A is provable.