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, 2022 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, 2022 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, 2022 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.


You must log in to answer this question.

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