Logical reasoning: What is the difference between NOT-elimination and False-introduction?

Question

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!

Answer 1

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:    ⊢ ⊥