0
$\begingroup$

I am new to mathematical logic so that maybe my problem is naive.

Consider a statement "$\forall n \in \Bbb{N},\ P(n)$" with a "checkable" property $P(n)$. In other words, there is a turing machine $M$ which can compute $P(n)$. If it is unprovable, then intuitively I think that it should be true, since any counterexample actually forms a proof of its incorrectness (correct me if I am wrong!).

So, I wonder that is there a concrete statement unprovably true in ZFC?

$\endgroup$
4
  • 2
    $\begingroup$ Check out Godel's incompleteness theorems. If ZFC is consistent, "ZFC is consistent" is a statement of the sort you want. $\endgroup$
    – Wojowu
    Commented Oct 22, 2017 at 15:01
  • $\begingroup$ I have found that the post mathoverflow.net/q/76897/22954 is useful for my question. So I would like to close this question. $\endgroup$
    – Lwins
    Commented Oct 22, 2017 at 15:11
  • 1
    $\begingroup$ Your intuition is correct (assuming, of course, that true arithmetic exists and is a model of the formal system of arithmetic one is using to form proofs, though an unprovable statement will necessarily also be false in some other, more exotic, nonstandard models of arithmetic). See the answers to mathoverflow.net/questions/27755/… $\endgroup$
    – Terry Tao
    Commented Oct 22, 2017 at 16:10
  • 1
    $\begingroup$ Something worth remembering is that "true" is meaningless without a proper context. In set theory, unlike arithmetic, there is no canonical model whose theory we take as "true". $\endgroup$
    – Asaf Karagila
    Commented Oct 22, 2017 at 19:53

0

Browse other questions tagged .