Gödel's famous incompleteness theorem implies, in particular, that there are statements unprovable in $\mathsf{ZFC}$. This implies that we could never hope to settle the truth of every mathematical statement using a reasonable (r.e.) axiom system, shattering Hilbert's program. However, in the 90 years since, many examples have been found of statements which are independent of the $\mathsf{ZFC}$ axioms.

Is it true (or possible) that any statement in $\mathsf{ZFC}$ (or another r.e. system $\mathsf{S}$) could be proven either:

  • true;
  • false;
  • independent of $\mathsf{ZFC}$ (resp. $\mathsf{S}$)?

This would allow a weak sort of realisation of Hilbert's program: for any statement, we can either prove/disprove it, or show it is independent of $\mathsf{ZFC}$.



The set of statements that is provably provable or provably refutable in $\mathsf{ZFC}$ is recursively enumerable but not recursive. If you could prove that the set of all statements independent of $\mathsf{ZFC}$ was determinable, it also would be recursively enumerable, but that's the complement of all statements that are either provably true or provably false, so the latter set would then be recursive, which it's not.

| cite | improve this answer | |
  • $\begingroup$ So there's an algorithm that iterates through all true statements of $\mathsf{ZFC}$? Can one give a description of it? $\endgroup$ – Jordan Mitchell Barrett May 13 at 7:00
  • 1
    $\begingroup$ You shouldn't use "provably true", but rather "provably provable". Likewise for "false". $\endgroup$ – Asaf Karagila May 13 at 7:14
  • $\begingroup$ @AsafKaragila I've made the change, but aren't they the same thing? A statement is provable if and only if it's true in all models of $\mathsf{ZFC}$. $\endgroup$ – Robert Shore May 13 at 10:40
  • $\begingroup$ Yes, and it is a common abuse of language to say "true in T" to mean "true in all models of T". But this trickles down, and eventually makes people talk about "truth". And whereas PA or other theories (RCF, ACF_0) have canonical models against which we test the notion of "true", ZFC does not have this property, so just talking about unqualified truth without having understood the context makes no sense. $\endgroup$ – Asaf Karagila May 13 at 10:42
  • $\begingroup$ @JordanMitchellBarrett Since $\mathsf{ZFC}$ has only countably many axioms and since all proofs are finite, you can just walk through all possible proofs from those axioms. $\endgroup$ – Robert Shore May 13 at 10:43

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