I am new to mathematical logic so that maybe my problem is naive.
Consider a statement "$\forall n \in \Bbb{N},\ P(n)$" with a "checkable" property $P(n)$. In other words, there is a turing machine $M$ which can compute $P(n)$. If it is unprovable, then intuitively I think that it should be true, since any counterexample actually forms a proof of its incorrectness (correct me if I am wrong!).
So, I wonder that is there a concrete statement unprovably true in ZFC?