3

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$
Vor
  • 690
  • 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 08: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 08: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 08: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 09:07
  • In that case, $\phi$ = "ZFC is inconsistent" still works. – Wojowu Apr 26 '18 at 09:10
  • @Wojowu: why? It seems that if we are on the $ZFC+Con$ "outer world", then if $\phi$ is "ZFC is inconsistent" then $ZFC+Con$ (Con added as an axiom) is already able to prove $\neg \phi$ even without the premise "ZFC proves that ..."? – Vor Apr 26 '18 at 09:18
  • You have said (in the last comment) that you wish to infer "ZFC proves $\neg\phi$". It is true that ZFC+Con proves $\neg\phi$, so what? – Wojowu Apr 26 '18 at 09:20
  • @Wojowu: yes sorry, I meant "conclude in ZFC+Con that $\neg \phi$". But you can post the first comment as an answer and I'll accept it. – Vor Apr 26 '18 at 09:25

1 Answers1

1

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.

Wojowu
  • 26,600