I am studying proof theory with Girard's monograph from '87 ('proof theory and logical complexity').
1.5.6. is an exercise called 'ordering between theories'.
It reads as follows:
" (i) Let $\textbf{G}$ be the set of all primitive recursive extensions of $\textbf{EA}$ containing $\textbf{PRA}$; define the following relation of $\textbf{G}$:
$$ \textbf{T} < \textbf{U} $$ if and only if $$ \textbf{U} \vdash (Con(\textbf{T})) $$
and show that < is irreflexive and transitive: < is a strict order.
(ii) Is it possible to have $\textbf{T}, \textbf{U} \in \textbf{G},\textbf{T} \vdash (Con(\textbf{U})) ,\textbf{U} \vdash (Con(\textbf{T})) $?
(iii) If $ \textbf{T} < \textbf{U} $ and $\textbf{T} \vdash A$, with $A$ a closed $\Pi^0_1$ -formula, show that $\textbf{U} \vdash A$."
I think (ii) is quite obviously impossible, since then by transitivity we would have a theory proving its own consistency, which is impossible by the second incompleteness theorem.
But I don't know how to deal with the transitivity from (i) or how to deal with (iii).
Thanks, Ettore
$\textbf{(Sketch of a) proof of transitivity (i):}$
We may suppose that $W$ is consistent, for if it is inconsistent it proves anything.
Assume $W \vdash Thm_U(0=1)$ - we're after a contradiction $in$ $W$.
We have $W \vdash Thm_U(0=1) \rightarrow Thm_T(Thm_U(0=1))$.
This is an instance of theorem 1.4.7., that is the formalization of 1.3.4. (iii).
Hence $W \vdash Thm_T(Thm_U(0=1))$.
Since $T \vdash \neg Thm_U(0=1)$, also $W \vdash \neg Thm_U(0=1)$. It think this is because if the statement is provable in some theory extending EA, it is provalbe in $any$ theory extending EA, but I am not sure.
So: $W \vdash Thm_T(\neg Thm_U(0=1))$. It think that should be possible for any theory T, as long as T is prim.rec.
Now, I guess it is not difficult to see that, although not sure about the precise way how to do it, from $W \vdash Thm_T(\neg Thm_U(0=1))$ and $W \vdash Thm_T(Thm_U(0=1))$, it follows that $W \vdash Thm_T (0=1)$.
But we already know from the beginning that $W \vdash \neg Thm_T (0=1)$.
So we get a contradiction in $W$ by assumption of $W \vdash Thm_U(0=1)$, thus we get $W \vdash \neg Thm_U(0=1)$.
It seems to me that a lack of my understanding comes from not really knowing what the provability predicate is able to do. It seems to me that my textbook didn't clarify these things very explicitly, or at least I didn't notice. Specifically the predicate was never used for different theories at the same time (in this intricated way).
$\textbf{Now an offer for a proof of (iii):}$
We head for a contradiction within $U$.
Suppose $U \vdash \neg A$.
$\neg A$ is a $\Sigma^0_1$ -sentence, since $A$ is a $\Pi^0_1$ -sentence.
Hence by theorem 1.4.7. (1.3.4. (iii) within PRA) $U \vdash \neg A \rightarrow Thm_T(\neg A)$, as $U$ contains PRA and $T$ extends EA, and thus $U \vdash Thm_T(\neg A)$.
But since $T \vdash A$, also $U \vdash Thm_T(A)$ by theorem 1.3.4., as long as $T$ is any prim. rec. theory and $U$ extends EA, since $Thm_T(A)$ is a true $\Sigma$ -sentence.
So by $U \vdash Thm_T(\neg A)$ and $U \vdash Thm_T(A)$ also $U \vdash Thm_T(\neg A \land A)$, that is $U \vdash Thm_T(0=1)$.
But we have as a premise that $U \vdash \neg Thm_T(0=1)$.
So we derived a contradiction in U from $U \vdash \neg A$. So $U \vdash A$.