It is more helpful to view "predicate logic" as a taxonomic term (the same goes for the term "logic" itself). So the question becomes: what properties of a logic cause us to call it a "predicate logic"?
That's a hard question partially because "logic" itself is so broad. We can identify at least a few common properties, but not every predicate logic will have all of them. The basic examples, of course, are the logics that are called "first-order logic" in the literature. But there are also higher-order logics, modal predicate logics, temporal predicate logics, etc.
Here are a few common traits:
Predicate logics may have variables to range over "individual" objects. There many be more than one sort of "individual".
Predicate logics may have variables that range over higher types or predicates, with syntax to match.
Predicate logics often have quantifiers over the individuals and other sorts of objects
Predicate logics often come with semantics in which the predicate symbols in formulas are interpreted as relations on a set of "individuals".
Yes, you can prove it with "usual" proof systems : Resolution, Tableaux or with Natural Deduction :
1) $∀z∀x∃y(R(z,y)∨¬P(x))$ --- premise
2) $∃xP(x)$ --- assumed [a]
3) $P(w)$ --- assumed [b] for $\exists$-elimination
4) $∃y(R(z,y)∨¬P(w))$ --- from 1) by $\forall$-elimination twice
5) $R(z,y)∨¬P(w)$ --- assumed [c] for $\exists$-elimination
6) $P(w) \to R(z,y)$ --- from 5) by tautological equivalence : $(p \to q) \leftrightarrow (\lnot p \lor q)$
7) $R(z,y)$ --- from 3) and 6) by $\to$-elimination
8) $\exists yR(z,y)$ --- from 7) by $\exists$-introduction
9) $\forall x \exists yR(x,y)$ --- from 8) by $\forall$-introduction : $x$ is not free in any "open" assumptions
$y$ is not free in 9); thus, we can apply $\exists$-elimination with 4), 5) and 9) and conclude with :
10) $\forall x \exists yR(x,y)$, discharging assumption [c].
In the same way, from 2), 3) and 10), discharging assumption [b] and concluding with :
11) $\forall x \exists yR(x,y)$.
Finally :
$∃xP(x) \to \forall x \exists yR(x,y)$ --- from 2) and 11) by $\to$-introduction, discharging assumption [a].
With a final application of $\to$-introduction we conclude with :
$∀z∀x∃y(R(z,y)∨¬P(x)) \to (∃xP(x) \to ∀x∃yR(x,y))$.
Best Answer
Your left- and right-side translations aren't consistent with each other: the right side should instead be "for some question, if I solved it, then I passed the exam". On both sides, we're describing a past event, perhaps due to incomplete knowledge rather than the marking rubric's specifications.
By correctly noting that $$(\forall x \phi(x) \Rightarrow C) \kern.6em\not\kern-.6em\implies (\exists x\phi(x) \Rightarrow C),$$ you are countering the false claim $$(\forall x \phi(x) \Rightarrow C) \equiv (\exists x\phi(x) \Rightarrow C),\tag2$$ which is a stronger claim than statement $(1).$
The forward direction of statement $(1)$ is troubling you, so let's prove it. Suppose that its LHS premise $(\forall x \phi(x) \Rightarrow C)$ is true; then either of these possibilities must be true:
passed the test:
then $(\phi(x) \Rightarrow C)$ is true, so $\exists x(\phi(x) \Rightarrow C)$ is true.
failed the test:
then, by letting $x=p$ be the missed question, $\exists x(\phi(x) \Rightarrow C)$ is vacuously true.