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