Write formally: The biggest prime number does not exist. Assume that all variables are positive integers.
This is my attempt to solve this problem.
Let $\pi(x) = \mbox{x is prime}$. Then,
$$\pi(x) = (\forall a)(a|x \Rightarrow (a=1 \lor a=x)) \land x \ne 1$$
And so, the solution will be:
$$(\forall p)(\pi(p)) (\exists P)(\pi(P) \land P > p)$$
What do you think of this solution? Is it good?
(A) Your suggested solution is not a well-formed formula. You mean, I think,
$$(\forall p)[\pi(p) \to (\exists q)(\pi(q) \land q > p)]$$
which says, assuming you are quantifying over numbers, for any number, if it is prime, there exists a number which is prime and bigger than it. You missed the crucial conditional. (Also, don't mix lower case and upper case variables when the same type of variable is in question -- in fact, the syntax of your language will normally fix that the first-order variables are all lower case.)
(B) But even corrected, this is strictly speaking at best a translation of "for any prime, there is a larger one", not of "the biggest prime doesn't exist". Those two claims are logically equivalent --- but just because claims are equivalent doesn't mean you ought to render them the same way into logical notation. (Compare: "snow is white" and "it isn't the case that it isn't the case that snow is white" are equivalent -- it doesn't mean that you should render them the same way!)
Standardly we translate existence claims using the existential quantifier (the clue is in the name), and so negations of existence claims with a negated existential quantifier. So we really want a translation starting '$\neg(\exists p)$'.
This, then, is better:
$$\neg(\exists p)[\pi(p) \land (\forall q)(q > p \to \neg\pi(q))]$$
There doesn't exist a prime number such that any number larger than it is not prime.
(C) A bonus exercise: in your favourite proof system for FOL, show those two wffs are inter-derivable!