Why isn't GL system of provability logic reflexive? Formula $\square p \rightarrow p$ (axiom T; corresponding to reflexive modal frames) is interpreted as "if p is provable, then p", or more precisely: for all realizations (all substitutions for $p$), $PA \vdash Bew(\ulcorner p \urcorner) \rightarrow p$ (PA is system whose provability we discuss, i.e. some standard first-order axiomatization of Peano Arithmetic).
Now if we forget the fact that T combined with Gödel-Löb axiom produces a contradiction-proving disaster, what I'm wondering is what is intuitively wrong with T? Because to me it seems perfectly obvious that if we have a proof of $p$, then we also have $p$, since $p$ is just the last step of the mentioned proof. How can we have a proof (in PA) of something that doesn't hold (in PA)? Since proof is nothing more than coded array of sentences, we can simply follow its steps and get to $p$. 
Even $\square \bot \rightarrow \bot$ seems ok: if we can prove $\bot$, then $\bot$ does hold in this system (it's not T's fault that we're dealing with inconsistent system).
I'm new to provability logic (just started reading The Logic of Provability) so I guess I'm overlooking something obvious. Thanks!
 A: This is an area where it is very easy to get oneself confused from lack of precision. You write ${\it Bew}(\ulcorner p\urcorner)$ without specifying which axioms $p$ is to be proved from, and that makes an important difference.
Let's first consider
$$ T_0(p) \equiv {\it Bew}_{PA}(\ulcorner  p \urcorner)\to p$$
There's nothing wrong with this; if we believe in Peano Arithmetic at all, it must be true in the standard model, and so in particular $PA+T_0$ is consistent. (In general I will tacitly assume that $PA$ is true and consistent).
On the other hand, individual instances of $T_0$ are not necessarily theorems of $PA$. Because of Gödel-Rosser's incompleteness theorem, there is a model of $PA$ in which ${\it Bew}_{PA}(\ulcorner  \bot\urcorner)$ is true. But that means that in that model $T_0(\bot)$ is false -- so it cannot be a theorem.
In fact, Löb's theorem shows that $T_0(p)$ is a theorem of $PA$ if and only if $p$ itself is.
Since $T_0$ is consistent with $PA$ (and even true), we can choose to adopt it as an axiom. We may then consider
$$ T_1 \equiv {\it Bew}_{PA+T_0}(\ulcorner  p\urcorner)\to p$$
The story of $T_1$ is then much the same as that of $T_0$: We can convince ourselves that it is consistent with $PA+T_0$, in fact true in the standard model, but not a theorem of $PA+T_0$. And we can then continue by induction to
$$ T_n \equiv {\it Bew}_{PA+T_0+T_1+\cdots+T_{n-1} }(\ulcorner  p\urcorner) \to p$$
for any finite $n$.
However, bad things happen if we attemt to "go to the limit" and consider
$$ T_\infty(p) \equiv {\it Bew}_{PA+T_\infty}(\ulcorner  p\urcorner)\to p $$
Note that instead of a limiting process we could have arrived at $T_\infty$ directly by being sloppy about the precise meaning of $\Box$ in the pithy formulation "take $\Box p \to p$ as an axiom".
First, it isn't immediately clear that $T_\infty$ is well-defined at all, but I think, without having checked the details, that one of the recursion theorems can produce a formula that meets the above specification. So let's put that objection aside.
It is a much more serious problem that $T_\infty$ directly implies that $PA+T_\infty$ is consistent! That means that $PA+T_\infty$ can prove its own consistency and (Gödel-Rosser again) this is an offense punishable by inconsistency. So $T_\infty$ is not consistent with $PA$.
If we unfold the construction in the proof of Gödel-Rosser, we would get a concrete $p_0$ such that $PA \vdash \neg T_\infty(p_0)$. But that is not very enligthening, so let's instead consider intuitively why our intuition that $T_n$ must be true doesn't work for $T_\infty$.
Suppose we have a proof of some sentence $p$ from $PA+T_\infty$; we wish to convince ourselves that then $p$ is indeed true. The proof is a certain finite sequence of formulas; we can check one by one that each of these formulas is true, given that all of the previous ones. Except, that is, if one of the formulas is an instance of $T_\infty$ and is justified by "that is an axiom". Since the truth of $T_\infty$ was what we were trying to argue for, we cannot just assume it at that point. And it won't work to attempt to justify it by induction either, because there is no guarantee that the proof the "inner" $T_\infty$ is applied to is shorter or simpler than the outer one. So we might find ourselves in an infinite ascent there.

In the first version of this answer I wrote $T_\omega$ instead of $T_\infty$, but arguably $T_\infty$ isn't really the limit of the $T_n$s. In fact, we can continue the $T_n$ sequence transfinitely to
$$ T_\omega \equiv {\it Bew}_{PA+T_0+T_1+\cdots+T_n+\cdots }(\ulcorner  p\urcorner) \to p$$
and indeed
$$ T_\alpha \equiv {\it Bew}_{PA+\{T_\beta\mid\beta < \alpha\} }(\ulcorner  p\urcorner) \to p$$
for as many ordinals as we can describe in $PA$ in the first place. Neither of these have the circularity problem that plague $T_\infty$.
