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?