Undecidable statement that doesn't involve infinity

Question

All statements independent of ZFC I'm aware of involve infinity.

Do we know any statement independent of ZFC of the form $\forall n \in \mathbb{N}: P(n)$ where $P(n)$ is disprovable if false? (In other words, an independent statement that could be disprovable by a counterexample).

If not, can we show that such a statement must exist? Can there be a consistent logical system in which such a statement cannot exist?

Answer 1

As mentioned in the comments, "ZFC is consistent" is itself such a statement (once properly expressed in the language of set theory). We can do even better, though: the MRDP theorem (or rather, its proof) shows that (assuming ZFC is consistent) there is a Diophantine equation $P$ with no solutions, which ZFC cannot prove has no solutions. This is about as concrete as it gets!

So no, incompleteness manifests at even the most concrete levels of mathematical propositions.

---

EDIT: Expanding a bit on my claim above:

The MRDP theorem does not directly imply my claim above - hence my parenthetical comment "or rather, its proof."

The proof of the MRDP theorem "goes through in PA" in a precise sense:

$(*)\quad$ For any specific $\Sigma_1$ sentence $\varphi$ in the language of arithmetic, we get a specific Diophantine equation $\mathcal{E}_\varphi$ such that PA proves that $\mathcal{E}_\varphi$ has a solution iff $\varphi$ is true.

Now take $\varphi$ to be "ZFC is inconsistent." Under reasonable assumptions - namely, the $\Sigma_1$-soundness of PA and the consistency of ZFC - we get the following:

• $\mathcal{E}_\varphi$ has no solutions (since ZFC is consistent), and hence PA (being $\Sigma_1$-sound) doesn't prove that $\mathcal{E}_\varphi$ does have a solution.

• On the other hand we clearly can't have PA prove that $\mathcal{E}_\varphi$ does have a solution, since then PA would prove the consistency of ZFC and hence be inconsistent (and this contradicts $\Sigma_1$-soundness, to put it mildly).

So the sentence "$\mathcal{E}_\varphi$ has no solution" is (under the reasonable assumptions above) true yet undecidable in PA.

The proof of $(*)$ is not easy (it consists of carefully analyzing the proof of the MRDP theorem, which is quite nontrivial) so I'm not going to go into it here. If one is interested, a separate question on the topic would be reasonable and I might answer it if I find the time; as far as I can tell this hasn't been asked at MSE before.