3
$\begingroup$

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$
$\endgroup$
8
  • $\begingroup$ No. Consider $\phi$ to be "ZFC is inconsistent". This implies that ZFC proves $\neg\phi$, but ZFC can't prove $\neg\phi$. $\endgroup$
    – Wojowu
    Apr 26, 2018 at 8:31
  • $\begingroup$ @Wojowu: thanks! What happens if I add the assumption ZFC is consistent ? (I should have added it to the premise) $\endgroup$
    – Vor
    Apr 26, 2018 at 8:49
  • $\begingroup$ 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". $\endgroup$
    – Wojowu
    Apr 26, 2018 at 8:51
  • $\begingroup$ @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$" $\endgroup$
    – Vor
    Apr 26, 2018 at 9:07
  • $\begingroup$ In that case, $\phi$ = "ZFC is inconsistent" still works. $\endgroup$
    – Wojowu
    Apr 26, 2018 at 9:10

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thanks! Are you aware of some conditions/restrictions on $\phi$ that make the above inference correct ? $\endgroup$
    – Vor
    Apr 26, 2018 at 9:41
  • $\begingroup$ I'm afraid I am not aware of any such conditions. $\endgroup$
    – Wojowu
    Apr 26, 2018 at 9:51

You must log in to answer this question.

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