I am not sure I can help here because I don't know what type of proof you are looking for.
In mathematical logic, there is a distinction between syntax and semantics. Syntax specifies which strings of characters are well-formed formulas and how to derive new formulas from old ones. It is relatively straightforward to encode syntax into a computer. In the end, it is just string manipulation subject to precise rules.
Semantics, on the other hand, is about meaning and truth/falsity of formulas. For example, a theorem from calculus can be written as a finite string that a computer can manipulate, but its meaning may involve real numbers, which is a (very) infinite set that cannot fit inside a computer.
If you are looking for a syntactic proof, then you must work with precise inference rules. Saying which formal system you are using is essential in order to get help because there are dozens of such systems, similar to how there are dozens of programming languages. If one asks for help with writing a program but does not specify the programming language, then the most he/she can get is some informal pseudocode.
This formula is known as the "Drinker's paradox". If one interprets the domain as the set of people in a bar and P(x) as "x drinks", then the formula claims that there is a person such that if he/she drinks, then everybody does. (It is called a paradox because at first glance it is surprising that every bar has such a "leader".) So the semantical proof of the formula goes like this. Either there is a person that does not drink, or there isn't. If x does not drink, then take him/her as the witness of ∃x. Indeed, P(x) is false and therefore the implication is true. If, on the other hand, there are no non-drinking people, then everybody drinks. In this case, take any person as x; the conclusion of the implication is true, and so the whole implication is.
It is not correct to say "solve a proof". One can solve a problem or come up with a proof. By the way, what does "with 0-premises" mean?I have the following proof to solve with 0-premises.
This formula is indeed semantically equivalent to the original one. However, if you are looking for a syntactic proof, you can't just shift from one to the other. Imagine that you need to explain to a dumb computer, who knows only primitive inference rules, how you do the transition.Which is otherwise written as
∃x¬P(x) v ∃x∀yP(y)
Also, in studying first-order logic, one usually assumes that domains are non-empty. In this case, ∃x∀yP(y) is semantically equivalent to ∀yP(y). Indeed, x does not occur (freely) in ∀yP(y), so one can instantiate it with any domain element.
This is not an instance of the excluded middle. Both disjuncts here are semantically equivalent to ∀y¬P(y).So I would start by assuming its negation and use the instance of excluded middle
¬∃xP(x) v ¬∃x¬∀y¬P(y)
Show Ex(Px -> Ay Py):
Toward a contradiction, suppose ~Ex(Px -> Ay Py).
So Ax(Px & ~Ay Py).
So Px & ~Ay Py.
Since x not free in any premise, we have Ax Px.
So Ay Py, which contradicts ~Ay Py.
Show Ex~Px v ExAy Py:
Suppose ~Ex~Px. Show: ExAy Py.
Since ~Ex~Px, we have Ax Px.
So Ay Py.
So ExAy Py.