How to deal with ¬∃ (negated existential quantifier) in a proof?

Question

I need to prove that the following premises lead to a contradiction.

1. ∀x (P(x) → Q(x))
2. ∃x ¬Q(x)
3. ¬∃x (¬P(x))

A couple of things are confusing me.

1. Does the first premise say that if x is a P then it is a Q, meaning there can still be x's that are not Ps
2. How do I deal with ¬∃ in a logic system? I know the equivalent of premise 3 is ∀x ¬(¬P(x)), But I assume I need to prove that if I wish to use it?

What makes it more confusing is that the whole question is only for 4 marks and I cannot see a solution that will use so few steps.

After some much needed sleep, the answer came easily

  1. ∀x (P(x) → Q(x))   --- Premise
  2. ∃x ¬Q(x)           --- Premise
  3. ¬∃x (¬P(x))        --- Premise
  |  4. x0 ¬Q(x0)       --- Assume
  |  5.  P(x0) → Q(x0)  --- ∀x elim 1
  |  |  6.  P(x0)       --- Assume
  |  |  7.  Q(x0)       --- → elim 6, 5
  |  |  8.  ⊥           --- ⊥ intro 7, 4
  |  9.  ¬P(x)          --- ¬ intro 6 - 8
  | 10.  ∃x (¬P(x))     --- ∃x into 9
  | 11.  ⊥              --- ¬ elim 10, 3
 12.  ⊥                 --- ∃x elim 4 - 11, 2

Answer 1

1. Indeed. A logical implication "p → q" is true if either p is false or q is true - in other words, it is only false if p is true but q false.

   This means that we can say that ∀ x; P(x) → Q(x) is equivalent to ∀ x; Q(x) ∨ ¬P(x): for every x either Q(x) has to be true or P(x) has to be false, or both.

2. In this case, you need to show that the system holds a contradiction. So, if you can arrive at ∃ x; ¬P(x), you have shown a contradiction with premise 3 and you are done.

Answer 2

Premise 3 is equivalent to ∀x ¬(¬P(x)), which is equivalent to ∀x P(x). With premise 1) follows ∀x Q(x), which contradicts premise 2, q.e.d.

Added due to @Keelan's remark.

ad your first question: Yes, your are right.

ad your second question: If no element x exists with F(x) true then for all elements x the property F(x) is false, hence ¬F(x) is true.