I am curious and trying to reason about what consequences we get if we use the predicate in the diagonalisation lemma as the provability predicate. I don't think I succeeded, I would appreciate if anyone could lend some help.

So here it is:

Suppose Pr is a provability predicate for a deductively defined theory T, where T is a theory satisfying the diagonalisation lemma. Suppose A is a FIXED POINT for Pr in T, that is, that $T\vdash Pr(\ulcorner A\urcorner)\equiv A$.

My question is: What can we say about the formula A? Is it provable in the theory T?

I tried to reason as follow: (To be honest I have not yet got the hang of it, I find this topic a bit confusing, so there should be many flaws in my reasoning, please kindly correct my mistakes)

Since $T\vdash Pr(\ulcorner A\urcorner)\equiv A$ so $T\vdash A$. In words, since T can show that $\ulcorner A\urcorner$ is provable iff $A$, so T can show A. So A is provable in T. I don't think it sounds correct, but I have no idea how to fix it.

Also, if anyone has any better way to understand the topic, I would be more than happy to learn.

Many many thanks in advance, I really appreciate any helps.


In general, $\text{PA} \not\vdash \text{Pr}_{\text{PA}}(\ulcorner A \urcorner) \rightarrow A$. If this were true, then $\text{PA} \vdash \text{Pr}_{\text{PA}}(\ulcorner \bot \urcorner) \rightarrow \bot$, i.e. $\text{PA} \vdash \text{Con}(\text{PA})$. Similarly goes for $T$. But in the case of fixed points, if $T \vdash \text{Pr}_T(\ulcorner A \urcorner) \rightarrow A$, then by Löb's theorem, we have $T \vdash A$. Löb's theorem is your friend here.

In general for fixed points, $A$ is not provable in $T$. It turns out that, actually, that fixed points for the formula $\neg\text{Pr}_T(x)$ are all equivalent to $\text{Con}(T)$ in $\text{PA}$.

Proof: Let $\text{PA} \vdash \varphi \equiv \neg\text{Pr}_T(\ulcorner\varphi\urcorner)$. Reasoning in $\text{PA}$:

  • Suppose $\varphi$. Then $\neg\text{Pr}_T(\ulcorner\varphi\urcorner)$. But then if $\neg\text{Con}(T)$, then $\text{Pr}_T(\ulcorner\varphi\urcorner)$, so $\text{Con}(T)$.
  • Suppose $\text{Con}(T)$, and for reductio, assume $\neg\varphi$. So $\text{Pr}_T(\ulcorner\varphi\urcorner)$. Since $\text{Pr}_T(\ulcorner\varphi\urcorner)$ is $\Sigma_1^0$, and it's true, we can prove it (in $\text{PA}$). Hence, $\text{Pr}_T(\ulcorner\text{Pr}_T(\ulcorner\varphi\urcorner)\urcorner)$. Furthermore, by our initial assumption, $\text{Pr}_T(\ulcorner\varphi \leftrightarrow \neg\text{Pr}_T(\ulcorner\varphi\urcorner)\urcorner)$. Since $\text{PA}$ is smart enough to reason about proofs, it follows from these that $\text{Pr}_T(\ulcorner\neg\varphi\urcorner)$. But then $\neg\text{Con}(T)$, contrary to our assumption.

The above proof strategy of reasoning in $\text{PA}$ is often a useful tool in dealing with these sorts of things. It works since $\text{PA}$ is extremely smart (it can capture a good chunk of number theory!), so it certainly understands how normal proofs work.


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.