According to Godel’s theorems, we know that some propositions are expressible in a sufficiently expressive logic system, that cannot be proven or disproven

We also have proofs that some statements cannot be proven or disproven in certain theories (eg. as the continuum hypothesis in ZFC, or the axiom of choice in ZF).

My question is, is there a statement P such as

  1. We cannot prove or disprove P
  2. We cannot prove or disprove that we cannot prove and disprove P
  3. we cannot prove or disprove (2.)
  4. we cannot prove or disprove (3.)


n. we cannot prove or disprove (n-1)

$\ldots$ and so on for all n

What would be necessary and/or sufficient conditions on a theory that has such statements?

  • $\begingroup$ In general, we cannot determine whether a statement is provable or disprovable in ZFC. If it is neither , it is even the rule that we cannot prove that within ZFC. $\endgroup$
    – Peter
    Feb 3 at 15:18
  • 1
    $\begingroup$ If we proved, inside the same system, that we cannot prove or disprove a statement, we would be proving that the system is consistent (since if it were inconsistent we could prove and disprove the statement). Which cannot be possibly done by Gödel's 2nd incompleteness theorem. (unless of course the system was inconsistent) $\endgroup$ Feb 3 at 18:13
  • $\begingroup$ I think you need to be more precise about the meaning of unprovability in each of your statements. Imagine the answer to your question is yes; how do we know that (1) is true, considering that (2) is true? Relatedly, consider the question "Is there an odd natural number that we can't prove is odd?". Without specifying what constitutes a proof of oddness for an arbitrary number $n$ (in particular, what syntactic features of the proof make it "about" $n$), it's unclear what's being asked. $\endgroup$
    – Karl
    Feb 4 at 8:28

1 Answer 1


We can construct an undecidable formula $\phi$ in the language of Peano Arithmetic (PA) such that

PA $\vdash\phi\leftrightarrow\neg\Box\phi$,

where $\Box$ is the provability operator.

Iterating on $\psi$ as $\phi\leftrightarrow\neg\Box\phi$

$\psi'$ as $\psi\leftrightarrow\neg\Box\psi$

$\psi''$ as $\psi'\leftrightarrow\neg\Box\psi'$ and so on,

we get a family of undecidable formulas on the assumption that PA is consistent.

Hence, any consistent and incomplete system that we can do these operations has to suffice. By an employment of Solovay's Arithmetical Completeness Theorem, the task might be simpler.


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.