I am wondering whether this is the right site to ask this question, but since it involves proof and diagonalisation, hopefully it is the right place.
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? Is it refutable in the theory T? (That is, is its negation provable in T?) Could it be either provable or refutable?
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.
To grasp the concept better, I think it is easier for me to think of an example, but I am still struggling to find one. I am trying to find examples of formulas which are fixed points for Pr in the theory of Peano Arithmetic.
What I can think of about properties of numbers are like eveness, primeness. So suppose Pr represents there is a proof that $\ulcorner A\urcorner$ is even, and A is "I am even". Is my example correct? Again, I am really doubtful about my own example.
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.