Why does this theory prove that it's not consistent? Say we have some theory $T$ such that $Th(A_E) \subseteq T$ where $A_E$ are the axioms of arithmetic. How do I show that 
(1) there are sentences $\varphi_1$ and $\varphi_2$ such that $Th(A_E) \vdash \varphi_1 \leftrightarrow \psi(\varphi_2)$ and $Th(A_E) \vdash \varphi_2 \leftrightarrow \neg \psi(\varphi_1)$, where $\psi(\alpha)$ represents that $\alpha$ is provable from $T$.
(2) That $T \vdash \varphi_1 \rightarrow \neg \rho$ where $\rho$ expresses that $T$ is not consistent.
Here are my thoughts:
(1) If we have that we can prove that $\varphi_1$ is unprovable and call that statement $\varphi_2$, then we see that $\varphi_1$ represents the statement that it is unprovable that we can prove $\varphi_2$ which seems to follow. I'm not sure how to formalize this reasoning and every attempt I make seems to result in my relying on the existence of either $\varphi_1$ or $\varphi_2$.
(2) If $\varphi_1$ and $\varphi_2$ are independent of $T$ (that is that we can neither prove nor refute them, which seems to be the case), then I don't see why the consistency of $T$ is compromised.
Any thoughts would be much appreciated.
 A: 
(1) there are sentences $\varphi_1$ and $\varphi_2$ such that $\text{Th(A}_\text{E}\text{)} \vdash \varphi_1 \leftrightarrow \psi(\varphi_2)$ and $\text{Th(A}_\text{E}\text{)} \vdash \varphi_2 \leftrightarrow \lnot \psi(\varphi_1)$, where $\psi (\alpha)$ represents that $\alpha$ is provable from $T$.

Godel's Diagonalization lemma states that for any unary predicate $P$, there is a constant predicate (sentence) D (and its numerical encoding $[D]$) such that
$$D \leftrightarrow P [D]$$
So (1) can be solved by generalizing that lemma to 2 unary predicates $P$ and $Q$ and establishing that, for any 2 such unary predicates, there is a constant predicate $D$ such that
$$D \leftrightarrow P[Q[D]]$$
and letting $\varphi_1$ be $D$ and $\varphi_2$ be $Q[D]$.
Define operation $S$ as necessary such that for any unary predicate $Y$ and any number $z$ it holds $S[Yz] = [Y[Yz]]$ (this is actually somewhat demanding, but it helps to establish that it is a primitive recursive operation and have it already established that all primitive recursive operations can be encoded into the logic).
Define unary predicate $Bz = P[Q[Sz]]$.
Then $B[Bx] = P[Q[S[Bx]]] = P[Q[B[Bx]]]$.  So $B[Bx]$ is the witness for $D$.

For part 2, we if can use that all $\Sigma_1$ statements $P$ have the quality that $\vdash P \to \psi(P)$ (this is not immediately obvious but it is a structurally inductively establishable theorem, details on pages 47 to 49 of George Boolos' Logic of Provability), then


*

*$\varphi_1 \to \psi(\varphi_2)$

*$\psi(\varphi_1) \to \lnot \varphi_2$

*$\varphi_1 \to \psi(\varphi_1)$

*$\lnot \varphi_2 \to \psi(\varphi_2)$


Combine those to get $\varphi_1 \to (\psi(\varphi_2) \land \psi(\lnot \varphi_2))$.
