1
$\begingroup$

Given a concrete mathematical statement, such as BSD conjecture(https://en.wikipedia.org/wiki/Birch_and_Swinnerton-Dyer_conjecture), do we know if it is provable?

$\endgroup$
  • $\begingroup$ I suspect the answer, in the vast majority of specific cases, is going to be, quite simply, "We don't." I've never heard of a non-independence result that doesn't itself discern whether the statement is true or false. I would be interested in finding out if such a thing exists - by the consistency theorem, you could start with two models, one of the statement and one of its negation, and try and derive a contradiction. $\endgroup$ – Dustan Levenstein Feb 7 '16 at 16:21
  • $\begingroup$ What do you mean by provable? If you mean does a proof exist - then it is just as hard as to prove conjecture. Only provably correct conjecture provably exist a proof. If you mean if it is possible to have a proof, however, then it is easy. The only thing that you cannot write a proof are "non-statements". For example, one cannot write a proof to "Good Morning", or "How are you" $\endgroup$ – Andrew Au Feb 7 '16 at 16:27
  • $\begingroup$ @AndrewAu I was thinking people are trying to prove BSD conjecture, but is it possible that the conjecture is not provable by Godel's incompleteness theorem? $\endgroup$ – Qixiao Feb 7 '16 at 17:46
  • $\begingroup$ A statement is not "provable" in and of itself. It is only provable relative to a particular axiom system. The most common way to show an axiom system doesn't prove a statement is to build a model of the system that doesn't satisfy the statement. For BSD there seems to be no specific reason to suspect it is unprovable from ZFC set theory. $\endgroup$ – Carl Mummert Feb 13 '16 at 13:34
  • 1
    $\begingroup$ In general, however, there is no algorithm that can decide whether arbitrary statements are provable from ZFC. They have to be considered on a case by case basis. $\endgroup$ – Carl Mummert Feb 13 '16 at 13:35
1
$\begingroup$

You're using the wrong term. You mean to ask whether we can tell if a conjecture is decidable, meaning that it is either provable or disprovable. But no we cannot tell whether a statement is decidable if the quantifier complexity is too high. Furthermore, it may be possible that even the decidability of a statement is itself undecidable! (See below for an example.)

First read https://math.stackexchange.com/a/1643073/21820, to ensure that you fully understand the import of Godel's incompleteness theorem. After that, consider the following. $\def\imp{\rightarrow}$

[We work in a meta-system and assume that $PA$ is omega-consistent.]

Let $φ = \square_{PA} Con(PA) \lor \square_{PA} \neg Con(PA)$. [So $φ$ expresses "Con(PA) is decidable over $PA$".]

If $PA \vdash φ$:

  Within $PA$:

    $\square Con(PA) \lor \square \neg Con(PA)$.

    If $\square Con(PA)$:

      $\neg Con(PA)$. [by the internal incompleteness theorem]

      $\square \bot$.

      $\square \neg Con(PA)$. [by (D1),(D2)]

    $\square \neg Con(PA)$. [by basic logic]

    $\neg Con(PA)$. [because $PA$ is omega-consistent]

  Contradiction. [with the external incompleteness theorem]

Therefore $PA \nvdash φ$.

If $PA \vdash \neg φ$:

  Within $PA$:

    $\neg \square Con(PA)$. [by basic logic]

    If $\square \bot$:

      $\square Con(PA)$. [by (D1),(D2)]

      Contradiction.

    $\neg \square \bot$.

    $Con(PA)$.

  Contradiction. [with the external incompleteness theorem]

Therefore $PA \nvdash \neg φ$.

Thus $φ$ is independent of $PA$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.