Skip to main content
2 of 4
added 2412 characters in body
Noah Schweber
  • 20.7k
  • 10
  • 111
  • 332

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.

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

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.

Noah Schweber
  • 20.7k
  • 10
  • 111
  • 332