Trying to understand self-reference as it relates to Godel's Second Incompleteness Theorem As noted in this post, I'm trying to understand how a sufficiently powerful consistent theory $T$ can prove statements about itself without contradicting Godel's Second Incompleteness Theorem.  Let $Prb_T \sigma$ represent $T \vdash \sigma$, $Cons T = \neg Prb(0=1)$.  I know that assuming $T$ is consistent, $T \vdash Cons T$ is a contradiction. I also know from this answer that $T \vdash \neg (0 = 1)$ is true. but what about:


*

*$T \vdash Prb_T Cons T$

*$T \vdash \neg(p \wedge \neg p)$

*$T \vdash Prb_T(\neg (p \wedge \neg p))$

*$T \vdash (Prb_T(Cons T) \rightarrow \neg Cons T)$

*$T \vdash (Prb_T(\neg(p \wedge \neg p)) \rightarrow \neg (p \wedge \neg p))$
I'm thinking that 4 and 5 are both formulazations of the theorem within $T$ so they are valid.  If that's correct then 1 should not be valid since it would imply $\neg (Cons T)$.  I'm not sure though about 2 and 3.
 A: Here $T$ is a sufficiently strong, effective theory of arithmetic,
$\text{Pvbl}$ is the formalized provability predicate of $T$, and $\text{Con}(T)$ is the formalized statement of $T$'s consistency. 
The case of #1,  $T \vdash \text{Pvbl}(\text{Con}(T))$, is interesting.
If $T$ is satisfied by the standard model of arithmetic, then we have for each $\phi$ that $T \vdash \text{Pvbl}(\phi)$ if and only if $T \vdash \phi$ (weaker assumptions on $T$ will also cause that equivalence to hold). By the second incompleteness theorem, it is impossible for $T \vdash \text{Con}(T)$. So if $T$ is sufficiently reasonable (e.g. if it is satisfied by the standard model), then we will have $T \not \vdash \text{Pvbl}(\text{Con}(T))$.  The usual term for this property is "soundness", and in particular the $T$ here would be sound for $\Sigma_1$ formulas such as $\text{Pvbl}(\phi)$. 
On the other hand, we know in general that $T \not \vdash \text{Con}(T)$. So $T + \lnot \text{Con}(T)$ is consistent.  Let $R = T + \lnot \text{Con}(T)$.  Then, for all $\phi$, we will have $R \vdash \text{Pvbl}_R(\phi)$, assuming that we take the "natural" effective axiomatization of $R$. 
The proof is as follows. First, $R \vdash \lnot \text{Con}(T)$, which means that $R \vdash \text{Pvbl}_T(\phi)$ for all $\phi$, because $R$ can formalize the usual arguments showing that every sentence is provable from an inconsistent theory. Second, $R \vdash \text{Pvbl}_T(\phi) \to \text{Pvbl}_R(\phi)$, because $T$ is a subtheory of $R$ and because we chose the axiomatization of $R$ so that $R$ can prove $T$ is a subtheory of $R$. 
So, if we take the $T$ in the question to be this $R$, we will have
$R \vdash \text{Pvbl}_R(\text{Con}(R))$. Of course, we do not have $R \vdash \text{Con}_R$. In particular, the theory $R$ is not satisfied by the standard model, even though it is consistent. This is because $R$ proves the existence of numbers (such as a coded proof of $\text{Con}(R)$) which cannot be found in the standard model. Even more precisely, the theory $R$ is not sound for $\Sigma_1$ sentences;
We can also see that $R$ proves $\lnot \text{Con}(R)$. This does not contradict anything - it is possible for a theory to "prove it is inconsistent", even if the the theory is actually consistent, as this example shows. 
So the answer to #1 is that more information about $T$ is needed to know whether $T \vdash \text{Pvbl}( \text{Con}(T))$. 
A: Carl has addressed the most interesting of the bullet points. To round out his answer:
2 is certainly true (via LEM), and 3 is true by reflection (if I prove $p$, then I prove that I prove $p$).
4 is indeed a formalization of Godel's theorem, and is true for sufficiently strong theories.
Finally, let's look at 5. 5 has the form $T\vdash \alpha\implies \beta$, where we already know (2) that $T\vdash\beta$. So, without any attention paid to $\alpha$, we know that $T\vdash \alpha\implies\beta$. So 5 is true, trivially.
