I'm trying to prove the following:

  1. ¬(A --> B) ⊢ ¬(¬A v B)
  2. ¬(¬A v B) ⊢ (A ^ ¬B)
  3. ∀x∀y(P(x, y) --> ¬P(x, y)) ⊢ ∀x¬P(x, x)

For the first two, I feel like the first step is try assume the contradiction, but I'm not sure where to go from there. For the third one, this is what I have:

  1. ∀x∀y(P(x, y) --> ¬P(x, y)) premise
  2. ∀y(P(a, y) --> ¬P(a, y)) ∀-elimination of line 1
  3. (P(a, b) --> ¬P(a, b)) ∀-elimination of line 2
  4. P(a, b) assumption
  5. ¬P(a, b) arrow-elimination of lines 3 and 4
  6. ∀x¬P(x, b) ∀-introduction for line 5
  7. ∀x∀x¬P(x, x) ∀-introduction for line 6
  8. ∀x¬P(x, x) ∀-elimination for line 7

but I don't know if my step 5 or step 7 work...

  • $\begingroup$ What are your rules for negation? $\endgroup$ – Doug Spoonwood May 1 '14 at 5:28
  • $\begingroup$ Which natural deduction system are you using? Are you allowed to use any tautology in your deduction? I ask this because, if yes, the first derivations is straightforward. $\endgroup$ – Nagase May 1 '14 at 5:29
  • $\begingroup$ intro/elimination of conditionals, disjunctions, conjunctions, negations, modus tollens...I can use things as long as I prove them as lemmas before hand $\endgroup$ – user146767 May 1 '14 at 6:00
  • $\begingroup$ The predicate logic proof has you generalizing on a letter used in an assumption. This isn't legal... en.wikipedia.org/wiki/Universal_generalization $\endgroup$ – Doug Spoonwood May 1 '14 at 19:21
  • $\begingroup$ @DougSpoonwood so how would I go about proving it? I realized that I couldn't do many of those steps, so I have no idea where to start ... $\endgroup$ – user146767 May 1 '14 at 19:31

For the first two, as you said, we proceed indirectly:

$1.~\lnot(A \rightarrow B) \vdash \lnot(\lnot A \lor B)$

enter image description here

$2.~\lnot(\lnot A \lor B) \vdash (A \land \lnot B)$

enter image description here

$3.~\forall x \forall y(P(x, y) \rightarrow \lnot P(x, y)) \vdash \forall x \lnot P(x, x)$

This version is a bit different from yours, but the general strategy is the same:

enter image description here


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.