Let $\mathscr{T}$ be the (countable) collection of all theorems provable in ZFC. Define an equivalence relation on $\mathscr{T}$ by $\phi\sim\psi$ iff $(\phi \iff \psi)$. In other words, two theorems are equivalent iff they are logically equivalent.

Then we can say $\mathscr{T}$ is the disjoint, countable union of equivalence classes of (equivalent) theorems, call them $E_i$. By the axiom of choice, there exists a set, $\mathscr{E}$, containing precisely one element (theorem) from each equivalence class: $\mathscr{E} = \{\phi_i : i = 1, 2, ...\}$, $\phi_i \in E_i$.

Now, two theorems $\phi$ and $\psi$ are contained in $\mathscr{E}$ iff they belong to disjoint equivalence classes. In other words, $\phi, \psi \in \mathscr{E}$ iff $\neg (\phi \iff \psi)$ iff $((\phi \wedge \neg\psi) \vee (\neg\phi \wedge \psi))$, in particular $\phi$ and $\psi$ cannot both be true, contradicting the fact that they are theorems.

  • 1
    $\begingroup$ With $\phi\iff\psi$ do you mean that the formulas are provably equivalent, or that they are equivalent in a model we consider? $\endgroup$
    – Wojowu
    May 19, 2015 at 18:00
  • 3
    $\begingroup$ Not all true statements are logically equivalent to one another (nor even provably equivalent to one another in $\mathsf{ZFC}$.) Also, the axiom of choice doesn't seem relevant here: theorems can be coded by natural numbers, which are wellordered. $\endgroup$ May 19, 2015 at 19:02
  • 3
    $\begingroup$ @Trevor: You know the proof of inconsistency is probably bad, when you realize that you proved a far far weaker system is inconsistent. :-) $\endgroup$
    – Asaf Karagila
    May 19, 2015 at 19:09
  • 2
    $\begingroup$ Another problem: you say "two theorems $\phi$ and $\psi$ are contained in $\mathscr{E}$ iff they belong to disjoint equivalence classes" -- but even if you mean two distinct theorems, the right-to-left implication will not be true (unless it is vacuously true because there is only one equivalence class.) $\endgroup$ May 19, 2015 at 19:15

3 Answers 3


You're tacitly assuming that $\mathscr{E}$ contains more than a single element.

But suppose that $\varphi$ and $\psi$ are theorems of $\mathsf{ZFC}$. Then in particular, in every single model $M$ of $\mathsf{ZFC}$, $\varphi$ and $\psi$ are true. As such, we find that $M\vDash (\varphi\leftrightarrow \psi)$ for every model $M$, so by Completeness we see that $\varphi\leftrightarrow \psi$ is a theorem of $\mathsf{ZFC}$. This implies that $\mathscr{E}$ consists of a single element, because there was only a single equivalence class to start with.

(EDIT: Here I'm assuming you mean "logically equivalent relative to $\mathsf{ZFC}$". Refer to Asaf's answer to understand the distinction.)

  • $\begingroup$ You are tacitly assuming that $\sim$ is defined as "logical equivalence over $\sf ZFC$" rather than "logical equivalence". But I agree that this is not entirely clear and open to interpretation. :-) $\endgroup$
    – Asaf Karagila
    May 19, 2015 at 19:00
  • $\begingroup$ @AsafKaragila Yes, you're right, that is what I assumed. I'm glad you addressed it in your answer, and I'll add an edit to my answer noting the assumption. $\endgroup$
    – Hayden
    May 19, 2015 at 19:07

Being logically equivalent is far far stronger than $\sf ZFC\vdash\phi\leftrightarrow\psi$.

Since the proof of equivalence can be non-trivial at all. For example, just to give an example, $\sf ZFC$ proves that the compactness theorem for FOL and Łoś's theorem are equivalent (like any two theorems of $\sf ZFC$); but $\sf ZF$ does not prove that at all. So the proof of the equivalence must in fact use the axiom of choice (and in turn be just the conjunction of two provable statements).

Your equivalence classes, if so, are of things which $\varnothing$ proves to be equivalent. But once you've added back the axioms of $\sf ZFC$ you changed the rules of the game, and "collapsed" the equivalence classes into one.


The answers already given are absolutely right, but another more basic issue shows up in your last paragraph: just knowing that $\varphi$ and $\psi$ are not "equivalent" (whether this means that they are not logically equivalent, or equivalent modulo some theory, does not matter), does not mean that $\varphi$ and $\neg\psi$ are equivalent.

That is: if we know that $\varphi\iff\psi$ is not a tautology (resp. theorem of ZFC), this does not mean that $\neg(\varphi\iff\psi)$ is a tautology (resp. theorem of ZFC).

This might sound like a violation of the Law of the Excluded Middle, but it's not: this arises from the conflation of proof and truth. Since we're talking about provability (either by $\emptyset$ or by $ZFC$), that means that we're living in the context of a modal logic (specifically, provability logic; see http://sartemov.ws.gc.cuny.edu/files/2012/10/Artemov-Beklemishev.-Provability-logic.pdf): in addition to the usual language of set theory, we also have a modal operator $\Box$, meaning "is a tautology" (or "is a theorem of $ZFC$"). The point is that $\Box$ is non-truth-functional: the truth value of $\Box\varphi$ does not depend only on the truth value of $\varphi$.

Using the modal language, your last paragraph should read: $$\varphi,\psi\in\mathcal{E}\implies \neg\Box(\varphi\iff\psi){\color{red} \iff}\Box\neg(\varphi\iff\psi)\iff\Box((\neg\varphi\vee\psi)\vee(\varphi\vee\neg\psi)),$$ but the red biconditional (specifically, the left-to-right direction) is false: we can't pass $\neg$ through $\Box$. For a concrete example, consider the continuum hypothesis CH: certainly $\neg\Box CH$, but also $\neg\Box\neg CH$ - $CH$ is independent, that is, neither provable nor disprovable from $ZFC$. If we could pass $\neg$ through $\Box$, this would of course be a contradiction; and the statement "$\neg$ passes through $\Box$" is precisely the statement "the system of axioms we are dealing with is complete," which is nuked by Godel.

  • $\begingroup$ A nit-pick: in your displayed equation, you seem to be repeating the OP's mistake of saying that for any two elements in the domain of the equivalence relation, they are both in the choice set if and only if they are inequivalent. $\endgroup$ May 19, 2015 at 19:31
  • $\begingroup$ Also, it might be worth pointing out that even if we were dealing with a complete theory, the argument would still be wrong for the reason that Hayden pointed out, namely that there would only be one equivalence class. (Here I am assuming, as you do in your answer, that "$\iff$" is supposed to be provable equivalence in the theory, rather than logical equivalence.) $\endgroup$ May 19, 2015 at 19:34
  • 1
    $\begingroup$ Derp, fixed. . . $\endgroup$ May 19, 2015 at 19:36
  • $\begingroup$ Aaaaaaaaaaargh! (You know what's better than ordinals? Colors.) $\endgroup$ May 19, 2015 at 19:37
  • $\begingroup$ I hate colors. Maybe that's why I was never big into Ramsey theory, partition calculus and infinitary graph theory... :-) $\endgroup$
    – Asaf Karagila
    May 19, 2015 at 19:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .