Suppose we are studying recursively axiomatizable first order theories in some metatheory (e.g. PA or ZF).

If we have a proof that a given recursively axiomatizable first order theory is complete and contains PA then we also get a proof that it is inconsistent by Gödel. Not all proofs of inconsistency are of this form.

Is there a complete recursively axiomatizable first order logic containing Peano arithmetic such that the shortest known proof of its inconsistency is of the form above?