Description
Using PBC
==
Proof by contradiction, like any other rule, can be used to justify claims. Subproofs can be confusing or require additional work. Therefore, PBC should be avoided if possible. When trying to prove a claim, there is a simple test on whether PBC should be used to prove the claim. Only in these cases should PBC be used:
1. The claim is just an atom i.e. p(x), or q
2. The top level of the claim is or i.e. (p->q) V r
3. The top level of the claim is the existential quantifier i.e. ∃ x p(x)
However sometimes, these can be justified without PBC. Sometimes these *can* be done directly. In any other case, there is a direct approach to build the claim using the previously justified claims.
Problems
==
1. (4 points) ∀ x ∀ y p(x, y) ⊢ ∀ y ∀ x p(x, y)
2. (5 points) ∃ x ∃ y p(x, y) ⊢ ∃ y ∃ x p(x, y)
3. (4 points) ¬(p → q) ⊢ p ∧ ¬q
4. (5 points) ¬∃ x p(x) ⊢ ∀ x ¬p(x)
If you have not read the above note on “Using PBC”, you should do so now.
5. (6 points) ¬∀ x p(x) ⊢ ∃ x ¬p(x)
6. (6 points) ¬∀ x p(x) → q(x) ⊢ ∃ x p(x) ∧ ¬q(x)
What to submit
==
Commit and push your project containing the solutions to your github repository (see videos) before the deadline. A good practice is to commit/push whenever meaningful progress is made (like you finish a question or fix a bug).
