I started out with Shawn Hedman's "A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computatibility, and Complexity" to learn the very basics. When I got to "Proof by Contradiction" derivation rule, I tried to derive the conclusion from the premises as an exercise, I got there via a different path, but I'm not sure if my solution is sound or wishful thinking.
This is from the book:
Premises: ∪ {F } ⊢ G
∪ {F } ⊢ ¬G
Conclusion: ⊢ ¬F
Line Statement Justification 1 ∪ {F} ⊢ G Premise 2 ∪ {¬G} ⊢ ¬F Contrapositive applied to 1 3 ∪ {F} ⊢ ¬G Premise 4 ∪ {¬¬G} ⊢ ¬F Contrapositive applied to 3 5 ⊢ ¬F Proof by cases applied to 2 and 4
and this is the route I took:
| Line | Statement | Justification |
|---|---|---|
| 1 | ∪ {F} ⊢ ¬G | Premise |
| 2 | ∪ {F} ⊢ (¬G v ¬F) | V-introduction applied to 1 |
| 3 | ∪ {F} ⊢ (G → ¬F) | →-definition applied to 2 |
| 4 | ∪ {F} ⊢ G | Premise |
| 5 | ∪ {F} ⊢ ¬F | →-elimination applied to 3 and 4 |
| 6 | ∪ {¬F} ⊢ ¬F | assumption |
| 7 | ⊢ ¬F | Proof by cases applied to 5 and 6 |