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$.) 

If you add to Peano arithmetic the negation of a theorem whose shortest proof is very long, then you've got it.
There can be no finite upper bound on the ratio of the length of the shortest proof of a theorem to the length of the theorem.  Suppose there were such a bound $B$.  Then, since only finitely many sequences of characters have length less than $B$ times the length of the proposed theorem, one could search through all of them, checking each to see whether it's a proof.  Then one would have an algorithm for checking theoremhood --- a known impossibility.  The set of theorems is recursively enumerable, but not recursive. 
