# Natural Deductions of Propositional Logic and Predicate Logic

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...

• What are your rules for negation? – Doug Spoonwood May 1 '14 at 5:28
• 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. – Nagase May 1 '14 at 5:29
• intro/elimination of conditionals, disjunctions, conjunctions, negations, modus tollens...I can use things as long as I prove them as lemmas before hand – user146767 May 1 '14 at 6:00
• The predicate logic proof has you generalizing on a letter used in an assumption. This isn't legal... en.wikipedia.org/wiki/Universal_generalization – Doug Spoonwood May 1 '14 at 19:21
• @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 ... – 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)$ $2.~\lnot(\lnot A \lor B) \vdash (A \land \lnot B)$ $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: 