Does there exist inconsistent axiom schemata which require arbitrary long proofs of their inconsistency? Fix a first-order language $\mathcal{L} = \{R\}$ whose signature consists of equality and another binary relation symbol $R$. For an axiom schema $A$ and a sentence $\tau$ in this language, we write $A \vdash_n \tau$ if there exists a proof of length $n$ of $\tau$ from $A$. Define the following invariant for a given axiom schema $A$:
$$\kappa(A) := \min\{n : \, \exists \tau \, (A \vdash_n \tau \text{ and } A \vdash_n \neg \tau)\}.$$
In other words, $\kappa(A)$ to be the smallest positive integer $n$ such that a contradiction can be proven from $A$ using proofs of length at most $n$. In particular, $\kappa(A)$ is finite if and only if $A$ is inconsistent.
Is $\kappa(A)$ unbounded as $A$ varies, i.e. is it true that, for each $N > 0$, there exist an axiom schema $A$ such that $\kappa(A) \ge N$?
 A: This depends on the precise proof system, and notion of proof length, that you use. For example, the proof system that allows you to deduce any valid conclusion in one step is certainly sound and complete, and provides a counterexample. 
But for any reasonable proof system, the answer will be yes: specifically, as long as the question $$\mbox{"Is there a proof of $\varphi$ from $A$ of length $\le n$?"}$$ is uniformly decidable in $\varphi, A, n$ (where $A$ ranges over finite sets of sentences), there will be arbitrarily hard-to-find inconsistencies. 
This follows immediately from the fact that the set of validities of first-order logic (with equality) in one binary relation symbol is undecidable. This, in turn, follows since we can convert an arbitrary (finite-language) structure into a directed graph in a natural way. Specifically: there is a computable procedure for turning $\mathcal{L}$-sentences into $\{R\}$-sentences (where $R$ is a binary relation symbol) which preserves entailment, for every finite language $\mathcal{L}$ (and indeed this is uniform in $\mathcal{L}$).

This can be a bit hard to see at first, so let me describe a couple examples:


*

*A unary relation. Suppose $M$ is a structure in the language $\{U\}$ containing a single unary relation. Then we can form a new $\{R\}$-structure $N$, whose domain is that of $M$ and so that $R^N=\{(a, a): M\models U(a)\}.$ This is kind of a trivial solution, though, and doesn't generalize well.

*Two unary relations. At this point we try a different tactic. Let $M$ be a $\{U, V\}$-structure, where $U$ and $V$ are unary relation symbols. Our $\{R\}$-structure $N$ has domain $M\sqcup\{a, b_1, b_2\}$ - we add three new elements. $a$ is used to name $U$, and $\{b_1, b_2\}$ is used to name $V$. Specifically, we set $$R^N=\{(a, a)\}\cup\{(b_1, b_2), (b_2, (b_1)\}\cup\{(a, x): x\in M, M\models U(x)\}\cup\{(b_1, y): y\in M, M\models V(y)\}.$$ Note that $a$ is identifiable as the only element $R$-related to itself, and $\{b_1, b_2\}$ as the only pair of elements $R$-related to each other in both directions.

*${}$A ternary relation symbol.${}$ This is the first nontrivial one, and the last one I'll do here. Suppose $M$ is an $\{S\}$-structure, where $S$ is a ternary relation symbol. The idea is as follows:


*

*$N$ will have two main kinds of elements, standing for elements of $M$ and triples of elements of $M$.

*In order to make sense of these, we'll need to be able to talk about the $i$th coordinate of a triple; and we'll need "yes" element to connect some triples to, in order to indicate of $S$ holds of that triple in $M$.

*So we're going to need a bunch of "labels", as we had above.

*Specifically, we let $N$ be the following: the domain of $N$ is $$M\sqcup M^3\sqcup (M^3\times \{1, 2, 3\})\sqcup \{a_1^1, a_1^2, a_2^2, a_1^3, a_2^3, a_3^3, a_1^4, a_2^4, a_3^4, a_4^4\}$$ and the relation $R^N$ is $$\{(a_i^k, a_j^k):i, j, k\in\{1, 2, 3, 4\}\}$$ $$\cup\{((p, q, r), (p, q, r, i)): p, q, r\in M, i\in\{1, 2, 3\}\}$$ $$\cup\{((p, q, r, i), a^i_j): p, q, r\in M, i, j\in\{1, 2, 3\}\}$$ $$\cup\{((p_1, p_2, p_3, i), p_i): i\in\{1, 2, 3\}\}$$ $$\cup\{((p, q, r), a_i^4): M\models S(p, q, r)\}.$$

*This is very messy, but the basic idea is the same as the two-unary-relation example. Again, each of the sets $\{a_1^1\}$, $\{a_1^2, a_2^2\}$, $\{a_1^3, a_2^3, a_3^3\}$, $\{a_1^4, a_2^4, a_3^4, a_4^4\}$ is identifiable in $N$. The remaining objets of $N$ break down into two "main" sorts (the triples $M^3$ and the individuals $M$) and three "auxiliary" sorts (the extended triples connected to the first, second, and third block of $a$s respectively). $R$ behaves as a "two-step projection map" from $M^3$ to $M$: to tell what the $i$th coordinate of $(p, q, r)$ is, we look at what individual the element $(p, q, r, i)$ is connected to, and we can find $(p, q, r, i)$ given $(p, q, r)$ since the $i$th block of $a$s is identifiable. Finally, the fourth block of $a$s serves as the test for whether a triple satisfies $S$.
At this point it should be relatively clear how the general reduction goes, as well as relatively clear that actually writing it down would be a pain. 
A: The Wikipedia article on Gödel's speed-up theorem shows how to construct a concrete example starting from PA or similar theories subject to the incompleteness theorems.
