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))$.
You got the right idea for part 1, but it is unusual to use the logical notation that you do: $\neg$, $\forall$, and $\exists$ are logical operators, but $\models$ is a metalogic symbol; purists will not like you mixing those up. So, it may be better to use the English 'some' and 'all' and 'not'
For part 2: here is where you use the result of part 1! In particular, in order to decide whether $\varphi$ is valid or not, you can decide whether $\neg \varphi$ is satisfiable or not: if $\neg \varphi$ is satisfiable, then $\varphi$ is not valid, but if $\neg \varphi$ is not satisfiable, then $\varphi$ is valid. And now you just combine that with Godel's completeness result (to be precise: the theorem that a statement is provable if and only if it is valid ... the more difficult 'if' part of which is the completeness theorem): if $\varphi$ is valid, then it is provable, and if $\varphi$ is not valid, then it is not provable.
So for that first part: if you have algorithm $\mathcal{A}$ that can figure put whether $\varphi$ is satisfiable or not for any $\varphi$, then design algorithm $\mathcal{B}$ that is trying to figure out whether $\varphi$ is provable or not as follows:
Take in $\varphi$
Negate $\varphi$
Call algorithm $\mathcal{A}$ with $\neg \varphi$
4a. If algorithm $\mathcal{A}$ says that $\neg \varphi$ is satisfiable, then print '$\varphi$ is not provable!'
4b. If algorithm $\mathcal{A}$ says that $\neg \varphi$ is not satisfiable, then print '$\varphi$ is provable!'
Best Answer
$$\fbox{Syntactically}~^{\dagger}$$
For (1), assume $Pa \lor Pb$. Suppose $Pa$, then $\exists xPx$ (by $\exists$-introduction). Similarly for $Pb$. Since $\exists xPx$ follows from both cases, conclude $\exists xPx$ (by $\lor$-elimination based on the first assumption and the two cases). This shows that $Pa \lor Pb \vdash \exists x Px$.
For (2), assume $\forall x Px$. Then, in particular you have $Pa$ (by $\forall$-elimination). Similarly for $Pb$. Conjoin $Pa$ and $Pb$ to get the desired conclusion. This shows that $\forall x Px \vdash Pa \land Pb$.
Assuming the proof system is sound, these will imply $Pa \lor Pb \models \exists x Px$ and $\forall x Px \models Pa \land Pb$.
$$\fbox{Semantically}~^{\dagger}$$
For (1), assume some model satisfies $Pa \lor Pb$. This means that either the object denoted by 'a' is in the interpretation of the predicate 'P' or the object denoted by 'b' is. In either case, we know that the interpretation of 'P' is non-empty, therefore the model also satisfies $\exists xPx$.
For (2), assume some model satisfies $\forall x Px \equiv \lnot \exists x \lnot Px$. Suppose, for contradiction, that this model also satisfies $\lnot Pa \lor \lnot Pb$. Suppose it satisfies $\lnot Pa$, then it satisfies $\exists x \lnot Px$, but this contradicts the first assumption. Supposing that it satisfies $\lnot Pb$ similarly leads to a contradiction. Since both cases of the hypothesis lead to a contradiction, it follows that the model actually satisfies $\lnot(\lnot Pa \lor \lnot Pb)$, which is equivalent to $Pa \land Pb$.
$\dagger$ Meaning proof-theoretically and model-theoretically, respectively.