Can the "proves consistent" relation be proven antisymmetric? By antisymmetric I mean there is not some chain of theories in which some theory proves other theories consistent which in turn prove it consistent.
If $\succ$ is the "proves consistent" relation:
$A\succ B\iff (A\models Con(B))\quad\forall A\forall B $
then I think antisymmetry is usually written as follows:
$A\succ B\land B\succ A\implies A=B\quad\forall A\forall B$
Can this be proven?
This is an inquiry motivated in part by learning that Gentzen's Consistency Proof is neither weaker nor stronger than PA, which suggests an ordering may not necessarily be implied by proving consistency.
It would seem to me that by Godel's imcompleteness theorem we're denied reflexivity:
$A\succ B\implies A\neq B$
which denies us the usual antisymmetry rule. But it seems this doesn't necessarily rule out antisymmetry provided we have transitivity. Because if $\succ$ were both transitive and symmetric, we might have the following contradiction:
$A\succ C\succ A \implies A\succ A\implies A\neq A$
$\therefore\nexists C\mid A\succ C\succ A$
Which fulfils the purpose of antisymmetry when we're denied reflexivity.
So the limit of what I can prove is that "proves consistent" is antisymmetric provided it is also transitive - which I have, as yet, no reason to believe it is.
The question is ill-posed until you specify the kind of systems you have in mind, and your definition of "Con", without which you cannot ask whether a system proves "Con" of some other system... $ \def\box{\square} \def\con{\text{Con}} \def\pa{\text{PA}} $
Henceforth I shall restrict to systems with proof verifiers that interpret arithmetic (described here) including not proving the translation of "$\bot$". This is because for systems that interpret arithmetic it makes sense to ask whether they prove $\con(T)$ for any given system $T$ with a proof verifier. I shall use the standard notation from provability logic for ease of reasoning and explanation. I shall also omit the translation for the interpretation of arithmetic, but you should be able to easily fill that in yourself.
As Mauro said in a comment, it cannot be that $A \succ B \succ A$ and $A = B$ for any such systems $A,B$, due to irreflexivity of $\prec$, which is a trivial consequence of the incompleteness theorem. So clearly antisymmetry is out of the question, unless as you point out we also have transitivity of $\prec$, which would make antisymmetry vacuously true.
Theorem: $\prec$ is in fact transitive.
Take any such systems $A,B,C$.
If $A \vdash \con(B) \equiv \neg \box_B \bot$ and $B \vdash \con(C) \equiv \neg \box_C \bot$:
Within $A$:
$\neg \box_B \bot$.
$\box_B \neg \box_C \bot$. [$A$ can check that $B$ proves $\neg \box_C \bot$.]
If $\box_C \bot$: [Namely, if $C$'s verifier terminates and accepts some proof of "$\bot$".]
$\box_\pa \box_C \bot$. [$A$ can prove by induction that $\pa$ can prove that termination.]
$\box_B \box_C \bot$. [$A$ can translate the termination proof in $\pa$ to a proof in $B$.]
$\box_B \bot$. [$A$ can combine the proofs of $\box_C \bot$ and $\neg \box_C \bot$ to get a proof of $\bot$ in $B$.]
Contradiction.
Therefore $\neg \box_C \bot$.
Therefore $A \vdash \con(C)$.
Another consequence of transitivity is that there is no cycle of such theories that prove each other's consistency in a cycle.