What can we say about a fixed point for a provability predicate in deductively defined theory that satisfies diagonalisation lemma

Question

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.

Answer 1

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.