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

  • 1
    $\begingroup$ Here is a hint that may help with transitivity ($W < T$ and $T < U$ implies $W < U$). We are assuming that these theories include PRA. So, for example, if $\lnot \text{Con}(W)$ then every one of these theories proves $\lnot \text{Con}(W)$. Remember $\text{Con}(W)$ is $\lnot \ulcorner W \vdash 0 = 1\urcorner$. Moreover, if $W \vdash 0 = 1$ then $U \vdash \ulcorner T \vdash \ulcorner W \vdash 0 = 1\urcorner \urcorner $. This is because there is a primitive recursive function that takes a $W$ derivation of $0 = 1$ to a $T$ derivation of $\ulcorner W \vdash 0 = 1\urcorner$. $\endgroup$ – Carl Mummert Dec 6 '18 at 11:59
  • 1
    $\begingroup$ I should have written $T < W$ and $U < T$ implies $U <W$ to match the rest of my comment. $\endgroup$ – Carl Mummert Dec 6 '18 at 14:43
  • 1
    $\begingroup$ Con(W) is a $\Pi^0_1$ statement, but you are circling around the right idea. If $\lnot \text{Con}(U)$ then $T$ would prove $\lnot \text{Con}(U)$. What we want is the formalization of that: $W \vdash \lnot \text{Con}(U) \to \ulcorner T \vdash \lnot \text{Con}(U)\urcorner$. $\endgroup$ – Carl Mummert Dec 6 '18 at 19:22
  • 1
    $\begingroup$ I was imagining a proof by contradiction in $W$ - show that, within $W$, $\lnot \text{Con}(U)$ leads to a contradiction, because $W \vdash \lnot \text{Con}(U) \to \ulcorner T \vdash \lnot \text{Con}(U)\urcorner$, and also $T > U$ leads to $W \vdash \ulcorner T \vdash \text{Con}(U)\urcorner$ , and from $\ulcorner T \vdash \text{Con}(U)\urcorner$ and $\ulcorner T \vdash \lnot \text{Con}(U)$, $W$ can prove $\lnot \text{Con}(T)$. $\endgroup$ – Carl Mummert Dec 7 '18 at 2:25
  • 1
    $\begingroup$ I think it will be a similar argument - $\lnot A$ is $\Sigma^0_1$, so $U \vdash \lnot A \to \ulcorner T \vdash \lnot A\urcorner$. If you like, you would be welcome to write an answer in the answer box below (rather in the question box) to record it for others. $\endgroup$ – Carl Mummert Dec 7 '18 at 12:40

$\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$.

  • 1
    $\begingroup$ For $W \vdash \text{Thm}_T(\lnot \text{Thm}_U(0=1))$, we have assumed $U <T$ so $T \vdash \lnot \text{Thm}_U(0=1)$ and we have $T \vdash \lnot \text{Thm}_U(0=1)$ implies $\text{EA} \vdash \text{Thm}_T(\lnot \text{Thm}_U(0=1))$. So we don't need to show or assume $W \vdash \lnot \text{Thm}_U(0=1)$. $\endgroup$ – Carl Mummert Dec 11 '18 at 14:40
  • 1
    $\begingroup$ For the next part, the key point is that if $T$ is any primitive recursive theory and $\phi$ is any sentence in the language, there is a primitive recursive function that takes two inputs - a $T$-proof of $\phi$ and a $T$-proof of $\lnot \phi$ - and returns a $T$-proof of $0=1$. The exact function depends on the formal deduction system being used, but the overall structure is to prove the tautology $\phi \to (\lnot\phi \to 0=1)$ and then use modus ponens twice. $\endgroup$ – Carl Mummert Dec 11 '18 at 14:42
  • 1
    $\begingroup$ Since $W$ extends PRA, if there is a primitive recursive procedure that takes a proof of one kind to a proof of a second kind, then the provability predicate of $W$ will be closed under that operation. For example $W \vdash [\text{Thm}_T(\phi) \land \text{Thm}_T(\psi)] \to \text{Thm}_T(\phi \land \psi)$.This is because we obtain the proof of $\phi \land \psi$ by doing a straightforward (primitive recursive) manipulation of the proofs of $\phi$ and $\psi$, which does not depend on what those proofs look like. $\endgroup$ – Carl Mummert Dec 11 '18 at 14:45
  • $\begingroup$ I think I understand. In your first comment you mean $W \vdash \text{Thm}_T(\lnot \text{Thm}_U(0=1))$ in the end instead right? As for Thm, so one could say that a primitive recursive function allows W to calculate proof-Gödelnumbers from other proof-Gödelnumbers for T without really needing to 'touch' the proofs or the provability of intermediate steps themselves. $\endgroup$ – Ettore Dec 11 '18 at 16:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.