Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

For every first-order sentence (in some vocabulary) $\varphi$ let us denote by $\varphi^+$ to the sentence (in the vocabulary of ZFC) expressing "$\varphi$ is logically valid (i.e., $\varphi$ is true in all first-order structures)".

My question concerns whether it is possible or not that there is some first-order sentence $\varphi$ such that $\varphi^+$ is undecidable in ZFC (i.e., $\text{ ZFC } \not \vdash \varphi^+$ and $\text{ ZFC } \not \vdash \neg \: \varphi^+$).

share|improve this question
Maybe this is related: math.stackexchange.com/questions/17212/… –  Apostolos Aug 9 '11 at 6:34
By logically valid do you mean $\varphi$ is a tautology? –  Asaf Karagila Aug 9 '11 at 6:52
@Asaf Karagila: boumol may be using the same convention I do, which is that only formulas in propositional logic can be "tautologies" and sentences in first-order logic that are true in every model are "logically valid". –  Carl Mummert Aug 9 '11 at 11:46
@Carl: Thanks! I was not aware of this convention. –  Asaf Karagila Aug 9 '11 at 11:50
@Carl: Thanks for replying Asaf (your convention is the same one I use). –  boumol Aug 9 '11 at 12:41
show 1 more comment

2 Answers

up vote 7 down vote accepted

Here is a concrete example of a $\phi$ such that neither $\phi^+$ or $\lnot (\phi^+)$ is provable in ZFC.

Let $\psi$ be the conjunction of the finite number of axioms of Goedel–Bernays set theory (NBG). Note that ZFC does not prove the consistency of NBG or the inconsistency of NBG. This follows from a conservation theorem that a sentence in the language of ZFC is provable in NBG if and only if ZFC proves that sentence; in particular NBG proves the sentence that says "0=1" if and only if ZFC proves that sentence. This conservation theorem is itself formalizable in ZFC, so ZFC proves that Con(NBG) and Con(ZFC) are equivalent.

Let $\phi$ be $\lnot \psi$. Thus $\phi$ is true in every structure if and only if $\psi$ is false in every structure, and this is also provable in ZFC. Also, ZFC is able to formalize the completeness theorem, so ZFC proves "$\psi$ is false in every structure if and only if $\psi$ is inconsistent".

Now, if ZFC proves $\phi$ is logically valid, then ZFC proves "NBG is inconsistent", which is impossible because NBG is consistent and ZFC is $\omega$-consistent. On the other hand, if ZFC proves $\phi$ is not logically valid, then ZFC proves there is a model of $\psi$, which is a model of NBG; this cannot be proved in ZFC because ZFC doesn't prove "NBG is consistent". This last step again uses the fact that the completeness theorem can be formalized in ZFC.

As with Levon Haykazyan's answer, I had to assume here that ZFC is ω-consistent to know that ZFC doesn't prove "NBG is inconsistent". Even if ZFC is only consistent, it can't prove "NBG is consistent", because (as above) ZFC can prove that Con(NBG) implies Con(ZFC), and the second incompleteness theorem requires just simple consistency to conclude that ZFC can't prove Con(ZFC).

share|improve this answer
Carl, $\lnot\phi^+$ is not too defined, do you mean $(\lnot\varphi)^+$ or $\lnot(\varphi^+)$? –  Asaf Karagila Aug 9 '11 at 12:24
In the original question, I assumed that it meant $\lnot (\phi^+)$, because the question was about whether $\phi^+$ could be proved or disproved in ZFC. –  Carl Mummert Aug 9 '11 at 12:28
Ah, I see you are correct. I need some sleep :-) –  Asaf Karagila Aug 9 '11 at 12:35
@Carl: Could you give some hint on what you mean by Morse-Kelley set theory? In its Wikipedia page it is said that "Morse–Kelley set theory cannot be finitely axiomatized", so it is not clear to me what formula is $\psi$. –  boumol Aug 9 '11 at 15:25
@boumol: I was thinking of Goedel-Bernays set theory, which can be finitely axiomatized, instead of Morse Kelley set theory. I edited the answer to fix that, and I tried to expand a little on the equivalence between Con(NBG) and Con(ZFC). –  Carl Mummert Aug 9 '11 at 17:00
add comment

The answer is yes. If for every $\varphi$, we have either $\rm ZFC \vdash \varphi^+$ or $\rm ZFC \vdash \lnot \varphi^+$, then we can have an algorithm for deciding whether $\varphi$ is logically valid or not. The algorithm will lookup for either a proof of $\varphi^+$ or $\lnot \varphi^+$ and will halt by the assumption. However, such an algorithm cannot exist by Church's theorem.

All this holds, provided ZFC is consistent and $\varphi^+$ can effectively be obtained from $\varphi$ (which I believe it can).

share|improve this answer
This is a nice argument (+1). I think it's worth noticing that this uses only the fact that ZFC is a true theory, and that the argument would apply equally well to any true theory which can formalize the statement "$\phi$ is logically valid" (which is equivalent, of course, to "$\phi$ is provable"). (P.S. Yes, a code for $\phi^+$ can be obtained uniformly effectively from a code for $\phi$. But the assumption needed on ZFC is stronger than just consistency.) –  Carl Mummert Aug 9 '11 at 11:40
Very nice (and simple) way to answer the question. Finally, I have chosen Carl's answer because it produces an example of such formula. –  boumol Aug 9 '11 at 18:22
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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