What is the difference between derivation rules: NOT-elimination and False-introduction?

My book says they are similar, but they differ in use. I think my book lacks the description of the difference and also when to use which one.

I hope someone can answer my question including a example!

  • Which book are you using? Mar 20 '14 at 1:25

The ¬-Elim says that:

If you have:                       ¬P ⊢ ⊥

Then you can conclude:   ⊢ P

Example. Suppose that 3 is not odd(¬O). Derive a contradiction using some number-theoretic fact (⊥). Then by ¬-Elim you can conclude that the assumption (viz. ¬O) was false, so O is the case.

Remark 1. Treating negation in a special way we get the equivalent form:

If you have:                       (P → ⊥) ⊢ ⊥

Then you can conclude:   ⊢ P

Combining this with the deduction theorem, we get the equivalent:

If you have:                       ⊢ (P → ⊥) → ⊥

Then you can conclude:   ⊢ P

Which, once the negation is re-interpreted in classical terms, becomes:

If you have:                        ⊢ ¬¬ P

Then you can conclude:    ⊢ P

Conclusion. ¬-Elim and the rule of "double negation elimination" are the same thing.

The ⊥-Intro rule says this:

If you have:                        ⊢ P   and   ⊢ ¬P

Then you can conclude:    ⊢ ⊥

Example. (this one is more abstract). Suppose that you have been able to derive that some number k is prime (P). If you have also been able to derive that that k has, say three divisors (¬P), then you can appeal to ⊥-Intro to conclude that you have derived a contradiction (⊥). You can then appeal to the fact that you have proved ⊥ to conclude any sentence Q you want (by ⊥-Elim).

Remark 2. The ⊥-Intro rule can also be seen as an instance of modus ponens (→-Elim):

If you have:                        ⊢ P   and   ⊢ (P → ⊥)

Then you can conclude:    ⊢ ⊥

  • Thanks for your explanation. But I meant the negation elimination, not the double negation elimination. Could you change your answer? My book says that one could conclude False from !P and P by both rules.
    – Tim
    Mar 19 '14 at 19:32
  • What does the Negation-Elimination rule say according to your book? Mar 19 '14 at 19:36
  • Okay, let me try something else. See if it's what you need. Mar 19 '14 at 19:41
  • It says: || || \n (k) !P \n || || \n P \n || || \n { !-elim on (k) and (l): } \n (m) False. Sorry for the \n, you would have to format it yourself. Also the ! should be the negation symbol. Looking at the False-introduction however it is completely the same, except the lines with || || consist of three vertical dots.
    – Tim
    Mar 19 '14 at 19:44
  • Check it out now. Mar 19 '14 at 19:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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