Natural deduction proof from falsehood

642 Views Asked by At

How does a proof of $⊥\rightarrow A$ (let $A$ be an arbitrary formula) look in the classical calculus of natural deduction?

1

There are 1 best solutions below

5
On

If you have a contradiction as a premise (or a correctly deduced conclusion from contradictory premises), then you are allowed to deduce anything you want through ⊥ elimination. Assuming a contradiction is no different than assuming what you want to conclude though, so I'm not sure what the point of assuming the contradiction is.

"Modern" logic:

If you want to show ⊥ → A, then simply start a subproof, then assume ⊥, use ⊥ Elim to get A, then end the subproof, and then use → Intro. As seen:

1|
 |----
2|| ⊥
 ||----
3|| A                           ⊥ Elim (2)
4| ⊥ → A                        → Intro (2-3)

Notice you don't need any premises for this proof.


Without using ⊥ Elim:

1|
 |----
2|| ⊥
 ||----
3||| ~A
 |||----
4||| ⊥                          Riet (2)
5|| ~~A                         ~ Intro (3-4)
6|| A                           ~ Elim (5)
7| ⊥ → A                        → Intro (2-6)

This also requires no premises.

You might be better off asking logic questions on the Philosophy StackExchange page: https://philosophy.stackexchange.com/