Is there a formula $\varphi (n)$ in one free variable $n$ in ZFC (PA etc.) such that for every formula $\psi(n)$ in one variable the equivalence
$$ \varphi ( \ulcorner\psi\urcorner) \leftrightarrow \neg \psi (\ulcorner\psi\urcorner) $$
is provable? Because this would imply the meta-equivalence
$$\vdash \varphi (\ulcorner\varphi\urcorner) \quad \Leftrightarrow \quad \vdash \neg \varphi (\ulcorner\varphi\urcorner) $$
so that the consistency of our formal system leads to neither $\varphi (\ulcorner\varphi\urcorner)$ nor its negation being provable.
My philosophy is: Formulas like $\psi (n)$ represent subsets of the natural numbers and gödelization seems to be an injection from the set of those formulas into $\mathbb{N}$. The $\varphi$ above corresponds exactly to the subset, that produces the contradiction in the proof of Cantor's theorem.
I once read a prove of the first incompleteness theorem but I remember the Gödel formula to be more complicate. What do you know about the suggested $\varphi$?
I also observe the resemblence between Cantor's theorem, the liar paradox, the Russel set and the Grelling–Nelson paradox. These paradoxes always arise if one considers properties of properties. Because a property can be associated to the class of all objects it holds for, the consideration of properties as objects, that can be inserted into properties, creates an injection from the totality of classes into the class of all objects and these injection, by Cantor's theorem, cannot exist. The paradoxes (Does a sentence holding for those sentences not holding for themselves hold for itself?, does a set containing those sets not containing themselves contain itself?, does a word describing those words not describing themselves describe itself?) now simply imitate the proof technique of Cantor's theorem. So I am interested if Cantor's theorem can be used to prove Gödel's inconsistency theorems.
Best Answer
Unless I'm missing something, this isn't possible unless the theory in question, which I'll call "$T$," is inconsistent: taking $\psi=\varphi$ we would have $$T\vdash (\varphi(\ulcorner\varphi\urcorner)\leftrightarrow\neg\varphi(\ulcorner\varphi\urcorner)).$$
That is, there is a sentence $\alpha$ (namely, $\alpha\equiv\varphi(\ulcorner\varphi\urcorner)$) such that $T\vdash (\alpha\leftrightarrow\neg\alpha)$. This clearly means that $T$ is inconsistent.
In a bit more detail, to make it clear that all rules are being followed, your assumption is that for each $\psi$ we have $$T\vdash (\varphi(\ulcorner\psi\urcorner)\leftrightarrow\neg\psi(\ulcorner\psi\urcorner)).$$ So taking $\psi$ to be $\varphi$ yields as a specific instance the contradiction-inducing sequent above; there's no need to pass to a "meta-equivalence."
Re: the role of diagonalization as a general framework for such arguments, see e.g. A universal approach to self-referential paradoxes, incompleteness and fixed points. My brief spiel on the matter would be that Lawvere's fixed point theorem has many such results as instances, but in no way "trivializes" them - you still need to set up the category in question and check its relevant properties. But there is definitely something real there.