# Hidden logic self-reference?

Let $\phi$ be a ZFC formula and $\lceil \phi \rceil$ its syntactic representation.

Suppose that

• ZFC proves that "if $\phi$ then there exists a string $x$ that represents a ZFC proof of $\lceil \neg \phi \rceil$ in some suitable proof system" ($x \equiv \lceil ZFC \vdash ^* \neg \phi \rceil$)

Can we conclude (by contradiction) that:

• ZFC proves $\neg \phi$
• No. Consider $\phi$ to be "ZFC is inconsistent". This implies that ZFC proves $\neg\phi$, but ZFC can't prove $\neg\phi$. – Wojowu Apr 26 '18 at 8:31
• @Wojowu: thanks! What happens if I add the assumption ZFC is consistent ? (I should have added it to the premise) – Vor Apr 26 '18 at 8:49
• What I've said still holds. Unless you mean replacing ZFC by ZFC+"ZFC is consistent"; for any theory T in place of ZFC subject to Godel's theorems we can consider $\phi$ to be "T is inconsistent". – Wojowu Apr 26 '18 at 8:51
• @Wojowu: adding the consistency I mean: Suppose that ZFC+Con proves that "if $\phi$ then there exists a string $x$ that represents a ZFC proof of $\lceil \neg \phi \rceil$ in some suitable proof system" can we conclude in ZFC+Con that "ZFC proves $\neg \phi$" – Vor Apr 26 '18 at 9:07
• In that case, $\phi$ = "ZFC is inconsistent" still works. – Wojowu Apr 26 '18 at 9:10

Here is a rather general answer. Let $T$ be any theory which is subject to the Godel's incompleteness theorems (for example, $T$ might be ZFC, as in the question, or ZFC+Con(ZFC) as discussed in the comments). Let $\phi$ be the statement "$T$ is inconsistent". Clearly $\phi$ implies that $T$ proves $\neg\phi$ (indeed, inconsistency of $T$ implies that $T$ proves anything). On the other hand, $T$ can't prove $\neg\phi$, because of the second incompleteness theorem. Hence we can't make the inference you are asking about.
• Thanks! Are you aware of some conditions/restrictions on $\phi$ that make the above inference correct ? – Vor Apr 26 '18 at 9:41