4 ms·
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 formu
by iamcurious 11y 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