Do there exist two formal systems, $F_1$ and $F_2$, such that $F_1$ proves $F_2$ is consistent and $F_2$ proves $F_1$ is consistent? Would these proofs bypass Gödel’s Second Incompleteness Theorem? By “consistent”, I mean the formal system does not prove $X$ and NOT $X$.
The answer to your question is no.
This stuff can be subtle! Let me first give an informal proof, and then expand it into an actual answer; without the informal proof, I’m worried that my rigorous argument will seem like spaghetti logic (proofs that use phrases like “… proves that … proves that …” are really hard to read without already knowing the main idea).
Informal proof: If $F_2$ is inconsistent, then $F_1$ knows it – a proof of a contradiction in $F_2$ can be verified by $F_1$. Since $F_1$ proves that $F_2$ is consistent, that means that if $F_2$ is inconsistent, then so is $F_1$ (since $F_1$ would prove both “$F_2$ is consistent” by assumption, and “$F_2$ is inconsistent” by the previous sentence).
Moreover, the above paragraph is pretty basic – in particular, $F_2$ can prove it! So $F_2$ proves “If $F_2$ is inconsistent, then $F_1$ is inconsistent”; or, in contrapositive, “If $F_1$ is consistent then $F_2$ is consistent.”
But $F_2$ proves “$F_1$ is consistent.” Combining the previous two sentences, $F_2$ proves “$F_2$ is consistent.” So Goedel’s Second Incompleteness Theorem goes CHOMP.
Alright, now let’s try to make that rigorous.
Let’s start by pointing out some missing assumptions, beginning with strength. Goedel’s theorems apply to sufficiently strong systems – there are weak systems which prove their own consistency because they fail to prove basic properties about provability. Using such a system as both $F_1$ and $F_2$ gives a positive answer to your question, but for a very silly reason. So we want to restrict attention to systems that are strong enough that the question is interesting; for instance, systems extending $PA$ (although this is massive overkill).
We also need to restrict attention to theories which aren’t too complicated: there are arithmetically definable theories which prove their own consistency!
Finally, going back to strength, we’re thinking about two theories which “look at each other”. It’s not enough for the theories in question to be strong; they have to know that they are strong. Specifically, we’re going to need one additional assumption, $(\dagger)$ : that $PA$ proves that the theories each extend $PA$. Call such a theory a visible extension of $PA$. (There are weird theories which do extend $PA$, but $PA$-unprovably so. Incidentally, for a really weird phenomenon around $(\dagger)$, see this delightfully-named paper of Visser.)
EDIT: It turns out that $(\dagger)$ isn’t necessary. However, since the proof of this is not trivial, I’m going to leave this answer as it is, and simply refer the reader to the improved result.
If we restrict attention to such theories, then the answer to your question is no.
The key point is the following:
$(*)\quad$ If $T$ is a theory extending $PA$, then $T$ proves every true $\Sigma_1$ sentence. Moreover, if $S$ is a recursively axiomatizable extension of $PA$ satisfying $(\dagger)$, then $S$ proves the previous sentence.
I won’t prove this fact here, but proofs can be found in various places. I’m currently searching for a good reference.
Note that the second sentence of the claim above presupposes that the first sentence is expressible in arithmetic. This might look dubious, since in general truth is not definable. However, definable truth predicates for restricted classes of sentences do exist; in particular, the set of true $\Sigma_1$ sentences is definable in arithmetic, by a $\Sigma_2$ formula.
Also, it’s worth pointing out that – as for Goedel’s Second Incompleteness Theorem itself – PA is overkill. Much weaker systems are sufficient.
We also observe:
If $W$ is a recursively axiomatizable theory and $\varphi$ is a sentence, then the sentence “$W$ proves $\varphi$” is $\Sigma_1$.
Indeed, provability assertions are the only kind of $\Sigma_1$ fact that we’ll be interested in here.
Now we’re ready to actually answer your question:
There are no theories $F_1, F_2$ which are consistent, recursively axiomatizable visible extensions of $PA$ which prove each others’ consistency.
Proof. I’ll go line by line. I’ll highlight two assumptions:
(1) $F_1$ proves that $F_2$ is consistent.
(2) $F_2$ proves that $F_1$ is consistent.
and two facts about provability:
(A) $F_i$ proves every true $\Sigma_1$ sentence, for $i\in\{1, 2\}$.
(B) $F_i$ proves that $F_j$ proves every true $\Sigma_1$ sentence, for $i, j\in \{1, 2\}$.
That is, (A) and (B) correspond to the first and second sentences of $(*)$, respectively.
So let’s go!
By (2) and (A), $F_1$ proves “$F_2$ proves $F_1$ is consistent.”
By (B), $F_1$ proves “If $F_1$ is inconsistent, then $F_2$ proves $F_1$ is inconsistent.”
By the previous two lines, $F_1$ proves “If $F_1$ is inconsistent, then $F_2$ proves “$F_1$ is consistent” and $F_2$ proves “$F_1$ is inconsistent”.
That is, $F_1$ proves “If $F_1$ is inconsistent, then $F_2$ is inconsistent.”
But by (1) and the contrapositive of the line above, $F_1$ proves “$F_1$ is consistent.”
. . . So $F_1$ is inconsistent by Goedel’s Second Incompleteness Theorem.