Return to Answer

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

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

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

This depends on the precise proof system, and notion of proof length, that you use. But for any reasonable one, the answer will be yes: as long as the question "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 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.