The good news about Herbrand Logic is that it is highly expressive. We can formalize things in Herbrand Logic that cannot be formalized (at least in finite form) in Relational Logic. For example, we showed how to define addition and multiplication in finite form. This is not possible with Relational Logic and in other logics (e.g. First-Order Logic).
The bad news is that the questions of unsatisfiability and logical entailment for Herbrand Logic are not effectively computable. Explaining this in detail is beyond the scope of this course. However, we can give a line of argument that suggests why it is true. The argument reduces a problem that is generally accepted to be non-semidecidable to the question of unsatisfiability / logical entailment for Herbrand Logic. If our logic were semidecidable, then this other question would be semidecidable as well; and, since it is known not to be semidecidable, then Herbrand Logic must not be semidecidable either.
As we know, Diophantine equations can be readily expressed as sentences in Herbrand Logic. For example, we can represent the solvability of Diophantine equation 3x2=1 with the sentence shown below.
∃x.∃y.(times(x, x, y) ∧ times(s(s(s(0))), y, s(0)))
We can represent every Diophantine equation in an analogous way. We can express the unsolvability of a Diophantine equation by negating the corresponding sentence. We can then ask the question of whether the axioms of arithmetic logically entail this negation or, equivalently, whether the axioms of Arithmetic together with the unnegated sentence are unsatisfiable.
The problem is that it is well known that determining whether Diophantine equations are unsolvable is not semidecidable. If we could determine the unsatisfiability of our encoding of a Diophantine equation, we could decide whether it is unsolvable, contradicting the non-semidecidability of that problem.
Note that this does not mean Herbrand Logic is useless. In fact, it is great for expressing such information; and we can prove many results, even though, in general, we cannot prove everything that follows from arbitrary sets of sentences in Herbrand Logic. We discuss this issue further in later lessons.