Is there a public key semantically secure cryptosystem for which one can prove in zero knowledge the equivalence of two plaintexts? If Alice encrypts two messages $a$ and $b$, such that $x=E(a)$, $y=E(b)$. Can Alice prove (without revealing $a$, $b$ or the private key) that $a = b$?

Obviously the proof must not be too long and it should be practical to compute and verify (either interactively or non-interactively).

This is possible for the Pohlig-Hellman symmetric cipher, even if the ciphertexts are encrypted with different keys. But P-H is not public key.

If such a cryptosystem exists (and it is commutative or provides public re-encryption),  then one of the limitations in Mental Poker protocols could be solved. The problem is the existence (or not) of a protocol that can provide both semantic security and abrupt drop out tolerance (without any threshold scheme).
Edit: It seems that the encryption needs to be deterministic to be able to support drop-out tolerance, and I see no way to overcome this. Without determinism, I was only able to veto the cards of a single player from a new deck.

See What is the theoretical and practical status of mental poker? for a related question.
Yes.  Such proofs are possible for El Gamal.

It involves a zero knowledge proof of equality of a discrete log, together with the homomorphic property of El Gamal encryption.

Recall that given $E(a)$ and $E(b)$, anyone can form $E(a/b)$ using the homomorphic property of El Gamal.  Suppose $E(a/b)=(r,s)=(g^k,h^k a/b)$ (where $g$ is the generator and $h$ is the public key).  Then proving that $a=b$ is equivalent to proving that $a/b=1$, i.e., that $(r,s)=(g^k,h^k)$ for some $k$, or in other words, that $(g,h,r,s)$ is a Diffie-Hellman 4-tuple.  There is a standard zero-knowledge protocol to prove this fact.  That's all you need.