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.