Why does this theory prove that it's not consistent?

Question

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.

Answer 1

(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))$.