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.


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.

  • $\begingroup$ Thanks for your example. By the way, now I believe there was some mistake in my first proof. Could you take a look at my addendum? $\endgroup$ – boumol Apr 8 '11 at 17:48
  • $\begingroup$ Sure; this version is what I assumed you meant. $\endgroup$ – Andrés E. Caicedo Apr 8 '11 at 18:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.