Inconsistent theory with uniformly long refutation? I understand that there are theorems in PA that necessarily require "very long" proofs; cmp. [1]. On the other hand it seems interesting to think about Life in an inconsistent world. 
So is it conceivable that a (non-paraconsistent) deductive system $S$ be inconsistent, yet any proof of the statement $A\wedge\neg A$ necessarily "very long"?
(If so, then define the girth of $S$ as the minimum length of such a proof — which by explosion must be independent of $A$.) 

Yes, of course it's conceivable.  Suppose we have a consistent system $S$ that has a short theorem $T$ whose shortest proof is very long.  Consider the inconsistent system $S'$ obtained from $S$ by adjoining the axiom $\neg T$.  From any proof of $A \wedge \neg A$ in $S'$ you can produce (without much increase in length) a proof of $T \implies (A \wedge \neg A)$ in $S$, and then a proof of $\neg T$ in $S$, so the original proof must have been very long.
