Two theories proving each others' consistency, take 2

This question is inspired by this previous question.

It is not too hard - although a bit subtle - to show that if $F_1, F_2$ are two theories in the language of arithmetic which

• are recursively axiomatizable,

• extend PA, and

• $(\dagger)$ PA proves that $F_1, F_2$ each extend PA,

then if $F_1\vdash Con(F_2)$ and $F_2\vdash Con(F_1)$ we have $F_1, F_2$ are inconsistent.

These hypotheses can be weakened in a few ways; my question is whether the third can be done away with completely:

Are there recursively axiomatizable theories $F_1, F_2$ extending $PA$ which are consistent, but which prove each others' consistency?

A brief word on why $(\dagger)$ appears necessary: the idea is to argue that if $F_1$ is inconsistent, then $F_2$ knows this, and moreover $F_1$ knows that. To do this, however, we need to argue that $F_1$ knows that $F_2$ proves every true $\Sigma_1$ sentence. Of course, if $F_2$ contains $PA$ then that is correct, but why should $F_1$ know it without $(\dagger)$?

EDIT: Let me clarify how there can be recursively axiomatizable theories which contain $PA$, but don't satisfy $(\dagger)$. First, note that the statement "$Prov_{PA}(\varphi)\implies Prov_T(\varphi)$ (in English, "$T$ contains $PA$") is not $\Sigma_1$, but rather $\Sigma_1\vee\Pi_1$; so while $PA$ does prove every true $\Sigma_1$ sentence, that doesn't help us here.

That said, how can we construct an example of a theory containing $PA$ but not "visibly"?

Fix an effective enumeration $\{\varphi_n: n\in\mathbb{N}\}$ of $PA$, and let $$T=\{\varphi_n: \mbox{there is no contradiction in $PA+Con(PA)$ of length $<n$}\}$$ (here it doesn't matter exactly how we define the length of a proof, so long as it is effective and there are only finitely many proofs of each length). Now, clearly (:P) this contains $PA$. But consider the theory $S=PA+Con(PA)+\neg Con(PA+Con(PA))$:

• $S$ contains $PA$, obviously.

• $S$ is consistent, as long as we assume some basic niceness (e.g. that $PA$ is true) - apply Goedel's Second to $PA+Con(PA)$.

• $S$ proves that $T$ is finite (since for some $n$ we find a contradiction in the theory $PA+Con(PA)$ of length $n$.

• $S$ proves that $PA$ is consistent.

• And, finally, $S$ proves that $PA$ is not finitely axiomatizable (this is a neat fact - if $PA$ is consistent, then it is not finitely axiomatizable, and $PA$ knows this).

So $S$ is a consistent extension of $PA$ which proves that $T$ is strictly weaker than $PA$; but then this means that $PA$ does not prove that $T$ is not strictly weaker than $PA$. So $T$ "invisibly" contains $PA$.

Aha! Rene Schipperus and I figured it out (see the comment thread above).

The answer is no: the requirement $(\dagger)$ that $F_1, F_2$ "visibly" contain $PA$ is unnecessary.

Here is why: the only time $(\dagger)$ was used in this answer was to show

$F_i$ proves that $F_j$ proves every true $\Sigma_1$ sentence

for $i, j\in\{1, 2\}$. But for this, it's enough for $F_i$ to prove that $F_j$ contains Robinson's Q, a much weaker theory than $PA$, since $PA$ (which $F_i$ contains) proves that $Q$ proves every true $\Sigma_1$ sentence.

So the real question is, "Can a theory invisibly contain $Q$?"

The answer to this is no, for a simple reason: $Q$ is finitely axiomatizable! This means that the statement "$F$ contains $Q$" is $\Sigma_1$ - by contrast, note that if we replace "$Q$" with a non-finitely-axioatizable theory $R$ (like, say, the weak arithmetic $R$ :P), the statement "$F$ contains $R$" is $\Pi_2$.

Why does this difference matter? Well, since $F_i$ contains $PA$, $F_i$ proves "any theory containing $Q$ proves any true $\Sigma_1$ sentence." And since $F_j$ contains $Q$, $F_i$ proves "$F_j$ contains $Q$" by the above paragraph. So we don't need any visibility assumption at all.