Proof Theory

Entailment

Herbrand entailment holds whenever every Herbrand model that satisfies the premises satisfies the conclusion. The natural question to ask is whether there is an algorithm that can be used to answer entailment queries, i.e. does a given set of sentences Δ entail a particular sentence φ? It turns out there is formally no such algorithm because Herbrand logic is expressive enough to encode Diophantine equations and their inverses, which is enough to ensure entailment is not semi-decidable. First we give the proof that shows entailment in Herbrand logic is undecidable; then we give the proof that shows entailment is not even semi-decidable. Both rely on Diophantine equations.

It is well known that solving Diophantine equations, i.e. determining whether a polynomial equation has integer roots, written P(x₁,...,x_n) = 0, is undecidable. Every such polynomial can be expressed using multiplication and addition. For example, 4x³y² + 1 is 4*x*x*x*y*y + 1. The proof of the undecidability of Herbrand entailment shows how to encode addition and multiplication.

Theorem (∀* |= ∃* is undecidable): Δ |= φ is undecidable.
Proof: The proof shows how to encode arithmetic: N is the set of natural numbers, represented in unary. Add(x,y,z) is true when x + y = z. Mult(x,y,z) is true when x * y = z.

N(0)
N(s(x)) ⇐ N(x)
Add(0,y,y)
Add(s(x),y,s(z)) ⇐ N(x) ∧ N(y) ∧ N(z) ∧ Add(x,y,z)
Mult(0,y,0)
Mult(s(x),y,w) ⇐ N(x) ∧ N(y) ∧ N(w) ∧ Mult(x,y,z) ∧ N(z) ∧ Add(z,y,w)

∃x₁...x_n.P(x₁,...,x_n,0)

Corollary (|= is undecidable): Δ |= φ is undecidable.
Proof: The special case defined in the last theorem is undecidable; thus, the problem in general is undecidable. ∎

Interestingly, we can also encode the statement that says there is no solution to the Diophantine. That problem is not semi-decidable (otherwise solving the Diophantine itself would be decidable), ensuring that Herbrand Entailment is not semi-decidable.

Theorem (∀* |= ∀* is not semi-decidable): Let Δ be a set of sentences in ∀*. Let φ be a sentence in ∀*. Δ |= φ is not semi-decidable.
Proof: Here we encode a problem that is not semi-decidable as an entailment query in Herbrand logic, with the required characteristics. More precisely, we encode the query that says a Diophantine has no solution: every candidate solution when plugged in is either less than 0 or greater than 0. Start with the axioms for less-than (lt), which are added to the axioms in the above proof.

lt(s(x),0)
lt(s(x),s(y)) ⇐ lt(x,y)
¬ lt(0,0)

∀x₁...x_ny. (P(x₁,...,x_n,y) ⇒ (lt(y,0) ∨ lt(0,y)))

Corollary (|= is not semi-decidable): Δ |= φ is not semidecidable.
Proof: The special case defined in the last theorem is not semi-decidable; thus, the problem in general is not semi-decidable. ∎

So in general, there is no algorithm for determining that Δ |= φ even if it is true. But, for a special case of Herbrand logic, entailment is semi-decidable. That fragment is semi-decidable because in it Herbrand entailment is equivalent to first-order entailment. We use |=_FO to stand for first-order entailment.

Theorem (∀* |= ∃* iff ∀* |=_FO ∃*): Let Δ be a set of equality-free, quantifier-free sentences and ψ be an equality-free, quantifier-free sentence. Δ |= ∃*.ψ if and only if Δ |=_FO ∃*.ψ
Proof: Below we use Δ ∪ ¬ψ as shorthand for Δ ∪ {¬ψ}.

Δ |=_FO ∃*.ψ
⇔ Δ ∪ ¬ψ is First-Order-unsatisfiable.
⇔ there is no Herbrand model of Δ ∪ ¬ψ. (By Herbrand's theorem, since Δ ∪ ¬ψ is quantifier-free and equality-free)
⇔ Δ ∪ ¬ψ is Herbrand-unsat.
⇔ Δ |= ∃*.ψ ∎

Corollary (∀* |= ∃* is semi-decidable): Let Δ be a set of equality-free, quantifier-free sentences and ψ be a quantifier free sentence. Δ |= ∃*.ψ is semi-decidable.
Proof: Since |= is equivalent to |=_FO, and the latter is semi-decidable, so is the former. ∎

Since for a problem to be semi-decidable, its complement must not even be semi-decidable, the theorem above implies |# cannot be semi-decidable for the special case of entailment queries in the theorem. Thus, in general, |# cannot be semi-decidable.

Corollary (Δ |# φ is not semi-decidable): Δ |# φ (or equivalently, Herbrand satisfiability) is not semi-decidable.
Proof: Because entailment and therefore unsatisfiability in the fragment with ∀* premises and ∃* queries is semi-decidable, satisfiability of that fragment must not be semi-decidable. Otherwise, both unsatisfiability and satisfiability would be decidable. Thus, because a special case of satisfiability or equivalently |# is not semi-decidable, in general, satisfiability cannot be semi-decidable. ∎

Herbrand logic in its most general form is thus incomputable: neither entailment nor its negation is semi-decidable. Consequently some true sentences require infinite proofs in Herbrand logic, making the logic inherently incomplete. (This assumes our definition of an inference system is one where checking whether a candidate proof actually proves a given query is decidable. Under this assumption, if every true sentence in a logic admits a finite proof, entailment is semi-decidable: (1) the set of all finite proofs is recursively enumerable, (2) checking whether a given proof proves the query under consideration is decidable, (3) thus, if there is a finite proof, there is always a semi-decision procedure for finding it. Since entailment is not semi-decidable, there must be true sentences without finite proofs.)

Herbrand logic is therefore more expressive than FOL. In FOL, we can encode a Diophantine, but because entailment is semi-decidable, we are ensured that there is no r.e. axiomatization of the negation of an arbitrary Diophantine since otherwise FOL would decide Diophantines, which clearly it can't. But, in Herbrand logic, we can encode both the Diophantine and its negation; obviously, the downside is that we lose semi-decidability of entailment. The benefit is that some theories that are not recursively enumerable in FOL appear to be finitely axiomatizable in Herbrand logic. See Goedel for more information.

Finite Herbrand Logic

Another way to cut up the space of sentences in Herbrand logic is on the basis of what kinds of constants exist in the vocabulary. If there are no functions, the logic becomes much simpler; all the negative results above require functions in the vocabulary.

Consider a vocabulary V without function constants. Recall we assume the set of constants in a vocabulary is always finite. The set of ground terms for V is then equal to the (by definition nonempty) set of object constants, which means the universe for every Herbrand model for V is finite. The set of ground atoms is also finite, which makes the set of all Herbrand models finite. We use the term Finite Herbrand Logic (FHL) to refer to this class of vocabularies.

Theorem (Finite Herbrand Logic Expressiveness): Finite Herbrand Logic has exactly the same expressiveness as Propositional Logic with a finite set of propositions.
Proof: Let Δ be a set of FHL sentences with vocabulary V. Invent a new propositional symbol for each ground atom in V. Ground Δ. Since the set of ground terms is finite, the grounding will produce only finite-length sentences. Replace each ground atom in that grounding with the appropriate propositional symbol. The result is a set of propositional sentences that has the same consequences as Δ modulo the ground atom rewriting. The other direction is obvious: each propositional symbol is a relation constant of arity 0. ∎

Corollary: Δ |= φ in Finite Herbrand Logic is decidable.
Proof: Entailment in propositional logic is decidable; hence, so is entailment in Finite Herbrand Logic. ∎

Corollary: Every theory in Finite Herbrand Logic can be finitely axiomatized.
Proof: It is sufficient to show every set of models can be finitely axiomatized. Every finite Herbrand model can be finitely axiomatized by conjoining all the ground literals true in the model. A vocabulary in finite Herbrand logic always has a finite number of models. Disjoining the finite axiomatizations for each of the models in the theory finitely axiomatizes that theory. ∎

That is not to say that computationally, Finite Herbrand Logic has exactly the same properties as propositional logic; all it says is the two logics can express the same logical theories. The structure in FHL may allow for more efficient representation or processing of those theories.

Some More Proof Theory

In light of the negative results above, namely that Herbrand logic is inherently incomplete, it is not surprising that Herbrand logic is not compact. Recall that Compactness says that if an infinite set of sentences is unsatisfiable, there is some finite subset that is satisfiable. It guarantees finite proofs.

Theorem (NonCompactness): Herbrand logic is not compact.
Proof: Consider the following infinite set of sentences.

p(a)
p(f(a))
p(f(f(a)))
p(f(f(f(a))))
...

Corollary (Infinite Proofs): In Herbrand logic, Some entailed sentences admit only infinite proofs.
Proof: The above proof demonstrates a set of sentences that entail ∀x.p(x). The set of premises in any finite proof will be missing one of the above sentences; thus, those premises do not entail ∀x.p(x). Thus no finite proof can exist for ∀x.p(x).∎

This statement in this Corollary was made earlier with the condition that checking whether a candidate proof actually proves a conjecture is decidable. There is no such condition on this theorem.

Skolemization is another mainstay of many logics that does not have the same effect in Herbrand logic.

Theorem: In Herbrand logic, Skolemization does not preserve satisfiability.
Proof: The following set of sentences are unsatisfiable.

p(a)
∃x.¬p(x)

p(a)
¬p(k) ∎

This result is not surprising given the dependence of Herbrand satisfaction on the vocabulary.

Model Theory

Model theory in Herbrand logic is much simpler than it is in first-order logic.

Unlike first-order logic where two models A and B can be equivalent with varying strengths, i.e. elementarily equivalent, secondarily equivalent, ..., isomorphic, and equal, there is no such hierarchy in Herbrand Logic. Two models either satisfy all the same sentences because they are the same exact model, or they disagree on some ground atom, i.e. one satisfies it, and the other satisfies its negation. Thus, the set of ground literals satisfied by a model uniquely identify it.

In our discussion of model theory, we use the usual notation for the set of models that satisfy a given sentence set Δ: Mod[Δ]. Also, the set of sentences true in all models in the set M is denoted as usual by Th[M].

Theorem: Let S be the set of ground literals satisfied by a Herbrand model M. S is satisfied by exactly one Herbrand model: M. Equivalently, Mod[Th[M]] = {M}.

Corollary: Loewenheim-Skolem-Tarski does not hold in Herbrand logic.
Proof: Loewenheim-Skolem-Tarski is a theorem in first-order logic that states if a set of sentences has a model of any infinite size, it has a model of every infinite size. Clearly this theorem does not hold in Herbrand logic, since every infinite model has countable size.∎

Unlike Finite Herbrand Logic, not all theories are finitely axiomatizable.

Theorem: Some Herbrand models are not finitely axiomatizable.
Proof: Consider a vocabulary with the set of terms {a, f(a), f(f(a)), f(f(f(a))), ...}, and a single, unary relation constant p. The set of all Herbrand models over this vocabulary is a subset of the ground atoms {p(a), p(f(a)), p(f(f(a)), ...}. There are 2^ω such subsets, which is uncountably infinite. Since there are only countably many sentences from a countable vocabulary, there are models without finite axiomatizations. ∎

More concretely, consider a model that encodes the digits of π, alternating between the positive literals and the negative literals.

Unless the digits of π are finitely expressible, this model has no finite description.