Of course, it follows from the negative solution to Hilbert's 10th problem (Putnam-Davis-Robinson-Matijasevic) that one can construct a specific diophantine equation P(x1,x2,...,xm)=0 for some m such that the solvability of this equation (over Z) is undecidable in ZFC. I actually think m, and the degree of P, can be made to be quite smallish.
It follows, of course, that the equation has no integer solutions (for if it had, this would have been easily demonstrable in ZFC). But ZFC is not capable of providing a proof of this fact (assuming that ZFC is consistent. If it's not then it can provide a proof of anything...)
