What can we say about a fixed point for a provability predicate in deductively defined theory that satisfies diagonalisation lemma 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.
 A: 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.
