Undecidability in ZFC

Question

I would like to know whether the following statement is true or not: there is some first-order formula $\varphi$ such that "$\varphi$ is valid in all finite structures" is true although not provable in ZFC (i.e., it is undecidable).

I have not been able to find anything similar in the literature, but on the other hand it seems to me that the proof I write next is OK.

Proof Sketch: By Trakhenbrot's Theorem, which is provable in ZFC, the set of finitely valid formulas is $\Pi_1$-complete. Thus, in ZFC we can prove that "there is some function $\sharp$ such that for every $\Pi_1$ arithmetical sentence $\varphi$ it holds that: $\varphi$ is true iff $\varphi^{\sharp}$ is finitely valid". In particular, if we take $\varphi$ as the $\Pi_1$-formula $Con(ZFC)$ (the one expressing the consistency of $ZFC$) we obtain (as a consequence of Gödel's Second Incompleteness Theorem) that "$Con(ZFC)^{\sharp}$ is finitely valid" is not provable (nor refutable) in $ZFC$.

Is this proof OK? Is the previous statement true? [Of course, all the time I assume $ZFC$ to be consistent]

In case the statement holds, I would like to know whether someone knows an explicit $\varphi$ with the previous property.

---

Addendum: I think that there has to be some wrong detail in the above proof, because I have not used the fact that $\sharp$ is computable. It seems to me that the mistake is done when I say: in ZFC we can prove that "there is some function $\sharp$ such that ...". I suppose that the existence of this function is not inside the ZFC model; due to the computability of $\sharp$ indeed what we know is that there is some syntactic procedure $\sharp$ such that in ZFC we can prove that "for every $\Pi_1$ arithmetical sentence $\varphi$ it holds that: $\varphi$ is true iff $\varphi^{\sharp}$ is finitely valid". The rest of the proof keeps as before.

Answer 1

Your argument looks correct to me. Here is one way of finding a $\varphi$ as you want:

As you mentioned, we are assuming that ZFC is consistent, of course; else, everything is provable.

Fix a recursive enumeration of the axioms of ZFC, and a coding of pairs of integers by integers. We denote the code of a pair $\langle a,b\rangle$ by $(a,b)$.

There is a Turing machine $U$ that with input $(a,b)$ returns $1$ if there is a proof of a contradiction from ZFC using only the first $b$ axioms that takes at most $b$ steps (in some formal proof systems that you fix beforehand). Else, it returns 0.

You can code your machine in a finite structure with universe $\{0,\dots,n\}$, as long as $n$ is sufficiently large (say $n\ge N$). (This takes a mild amount of work but most books that discuss finite model theory explain how things like this can be done.)

You can then take $\varphi$ to say that either the size of the universe is $<N$, or else for all $i\le N$, the machine will return $0$ with input $(i,N)$. Note that $\varphi$ is $\Pi_1$.

Also, $\varphi$ is true, but ZFC cannot prove it, since proving $\varphi$ verifies the consistency of ZFC.