Assume we have some statement called $\alpha$. We will define a new statement $P(\alpha):="(\alpha\text{ can be proved})\lor(\lnot\alpha \text{ can be proved})"$

I claim that $P(P(\alpha))$ is always correct (that is, we can always prove\disprove whether a statement can be proved or not).

The following is a "proof" for that:

Assume towards contradiction that $P(P(\alpha))$ is not correct. Then, there is no proof for $P(\alpha)$ and also there isn't a proof for $\lnot P(\alpha)$.

Lemma: If $\alpha$ can be proved, say using some proof $p_\alpha$, then this $p_\alpha$ also proves that "$\alpha$ can be proved", hence $p_\alpha$ proves that $P(\alpha)$ is also true.

Use this lemma again and get that $P(P(\alpha))$ is true.

If $\alpha$ cannot be proved, then either that $\lnot\alpha$ can be proved or not. If it is possible to prove $\lnot \alpha$, then by the lemma we know that $P(\lnot\alpha)$ can be proved. But notice that by the definition of $P$ we have $P(\alpha)\equiv P(\lnot \alpha)$, so also $P(\alpha)$ can be proved, and once again, using the lemma we get that $P(P(\alpha))$ is true.

If its also impossible to prove $\lnot\alpha$, then by the definition of $P(\alpha)$ we have $P(\alpha)$ is false. However the "proof" up until this point proves that $P(\alpha)$ was false, since we assumed that there is no proof for $P(\alpha)$ but in every other case there was a proof. Thus, a contradiction - and hence $P(P(\alpha))$ must be true in this case as well.

My question

  1. Is this idea "correct"?
  2. If it is "correct", then is it possible to formalize it? how would it look like?

2 Answers 2


I feel like there is a kind of circularity in the last part of your argument (and I think the conclusion is wrong, there are undecidable problems which we cannot prove to be undecidable).

You are basically making a case distinction:

  • if $\alpha$ can be proved or $\neg \alpha$ can be proved: Then $P(\alpha)$ can be proved and thus $P(P(\alpha))$ is true. (I agree here)
  • if neither $\alpha$ nor $\neg \alpha$ can be proved: Then $\neg P(\alpha)$ can be proved and thus $P(P(\alpha))$ is true. I disagree here. The correct assumption to make this conclusion would be: "if we can prove that neither $\alpha$ nor $\neg \alpha$ can be proved".

Note that you cannot in general prove that you are in the second case. You say you can because otherwise you could prove that you are in the first case. But what you need is to be able to prove that you cannot find a proof that you are in the first case, which is a different thing.

  • $\begingroup$ Maybe I phrased it wrong. What I meant is that if $P(\alpha)$ cannot be proven, then we are not in any one of the cases above (since there $P(\alpha)$ can be proved). Thus, both $\alpha$ and $\lnot \alpha$ cannot have proofs, and therefore we proved that $P(\alpha)=false$ hence we proved that $P(P(\alpha))$ is also true. I might agree that this is a bit circular, but that is exactly why I asked this question in the first place $\endgroup$
    – nir shahar
    May 26, 2021 at 21:18
  • $\begingroup$ And about undecidability, its a bit different from having a proof. Even if something is undecidable, for every specific instance of the problem, the answer can be known (and there might even be a proof for that). Does undecidability mean that there is an instance without a proof? From my knowledge finding a proof is only an $RE\setminus R$ problem so it doesn't guarantee us there isn't a proof. $\endgroup$
    – nir shahar
    May 26, 2021 at 21:22
  • $\begingroup$ @nirshahar There does not even have to be a notion of instance, I'm talking about undecidability of a statement in general, not necessarily related to computation. Like the continuum hypothesis is undecidable in ZFC. I maintain that what you are sating requires one to be able to prove that we are in the second case of the case distinction, not simply being in that second case. Just because you cannot find a proof for $\alpha$ nor $\neg \alpha$ doesn't mean that you can prove this fact. $\endgroup$
    – Tassle
    May 26, 2021 at 21:34
  • $\begingroup$ I think I got you. Thanks! $\endgroup$
    – nir shahar
    May 27, 2021 at 7:17

To reason safely about provability, you need to fix some kind of formal proof system. It usually won't matter at all what system you pick (barring some basic sanity checks), but it is important that "proving" should mean the same thing everywhere in your argument.

Here, "proof" in the last paragraph suddenly jumps from referring to whatever notion of proof you started with to some informal meta-reasoning, and that is where it all goes wrong.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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