formally prove ¬∀x:X.P → Q ⊣⊢ ∃x:X.¬(¬Q → ¬P)

Question

For formal proofs, would the negation from the universal need to be removed first? Would this be done by attempting to prove that ¬∀x:X.P → Q is also not true using negation induction?

that is to arrive to two opposite conclusions using the above proof? Right to left is easier to breach but left to right is leaving me puzzled.

Answer 1

This is based purely on what I managed to figure out, by backing up and not swapping the negative universal to an existential. ¬∀x:X.P → Q ⊣⊢ ∃x:X.¬(¬Q → ¬P)

1. ¬∀x:X.P → Q  (hyp)
  2. ¬Q → ¬P (assume)
  3. ¬∀x:X.P → Q (copy 1)

  4. ¬Q → ¬P (assume)
  5. P → Q (contrapositive, 4)
  6. ∀x:X.P → Q (∀ intro, 5)
7. ¬(¬Q → ¬P) (¬ intro, 2-3, 4-6)
8. ¬(¬Q → ¬P)[x/x] (A[x/x] = A)
9. ∃x:X.¬(¬Q → ¬P) (∃ intro, 8)

I'm not sure if this is the correct solution, but based on using the simplest rules possible, this is what I ended up with.

Primary Concern is whether or not line 3 and line 6 are truly opposites or if that doesn't count as a solid basis for introducing a negation as I did in line 7.

I would appreciate input on this answer.

Answer 2

Here is a proof with Natural Deduction; for the rules, see e.g.;

• Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), page 222.

1) $¬∀x(Px → Qx)$ --- premise

2) $¬∃x¬ (¬Qx → ¬Px)$ --- assumed [a]

3) $¬(¬Qx → ¬Px)$ --- assumed [b]

4) $∃x¬ (¬Qx → ¬Px)$ --- from 3) by $∃$-intro

5) $\bot$ --- from 2) and 4) by $\lnot$-elim

6) $¬Qx → ¬Px$ --- from 3) and 5) by Double Negation-elim, discharging [b]

7) $Px → Qx$ --- from 6) by Contraposition [it is easily proved with a sub-derivation]

8) $∀x(Px → Qx)$ --- from 7) by $∀$-intro : no open assumptions with $x$ free

9) $\bot$ --- from 1) and 8)

10) $∃x¬ (¬Qx → ¬Px)$ --- from 2) and 9) by Double Negation, discharging [a].

Thus, from 1) and 10) we have :

$¬∀x(Px → Qx) \vdash ∃x¬ (¬Qx → ¬Px)$.