Suppose we are studying first order theories in some metatheory (e.g. PA or ZF).
If we have a proof that a given 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 first order logic containing Peano arithmetic such that the shortest known proof of its inconsistency is of the form above?