Herbrand Logic
 
Proof TheoryThe Proof theory for Herbrand logic is much different than the proof theory for firstorder logic. The Model theory is also quite different. The proof theory is more complicated, and the model theory is much simpler.EntailmentHerbrand 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 semidecidable. First we give the proof that shows entailment in Herbrand logic is undecidable; then we give the proof that shows entailment is not even semidecidable. 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_{1},...,x_{n}) = 0, is undecidable. Every such polynomial can be expressed using multiplication and addition. For example, 4x^{3}y^{2} + 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.
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)
Corollary (= is undecidable): Δ = φ is undecidable.
Interestingly, we can also encode the statement that says there is no solution to the Diophantine. That problem is not semidecidable (otherwise solving the Diophantine itself would be decidable), ensuring that Herbrand Entailment is not semidecidable. Theorem (∀* = ∀* is not semidecidable): Let Δ be a set of sentences in ∀*. Let φ be a sentence in ∀*. Δ = φ is not semidecidable.
lt(s(x),s(y)) ⇐ lt(x,y) ¬ lt(0,0)
Corollary (= is not semidecidable): Δ = φ is not semidecidable.
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 semidecidable. That fragment is semidecidable because in it Herbrand entailment is equivalent to firstorder entailment. We use =_{FO} to stand for firstorder entailment. Theorem (∀* = ∃* iff ∀* =_{FO} ∃*): Let Δ be a set of equalityfree, quantifierfree sentences and ψ be an equalityfree, quantifierfree sentence.
⇔ Δ ∪ ¬ψ is FirstOrderunsatisfiable. ⇔ there is no Herbrand model of Δ ∪ ¬ψ. (By Herbrand's theorem, since Δ ∪ ¬ψ is quantifierfree and equalityfree) ⇔ Δ ∪ ¬ψ is Herbrandunsat. ⇔ Δ = ∃*.ψ ∎ Corollary (∀* = ∃* is semidecidable): Let Δ be a set of equalityfree, quantifierfree sentences and ψ be a quantifier free sentence. Δ = ∃*.ψ is semidecidable.
Since for a problem to be semidecidable, its complement must not even be semidecidable, the theorem above implies # cannot be semidecidable for the special case of entailment queries in the theorem. Thus, in general, # cannot be semidecidable. Corollary (Δ # φ is not semidecidable): Δ # φ (or equivalently, Herbrand satisfiability)
is not semidecidable.
Herbrand logic in its most general form is thus incomputable: neither entailment nor its negation is semidecidable. 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 semidecidable: (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 semidecision procedure for finding it. Since entailment is not semidecidable, 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 semidecidable, 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 semidecidability 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 LogicAnother 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.
Corollary: Δ = φ in Finite Herbrand Logic is decidable.
Corollary: Every theory in Finite Herbrand Logic can be finitely axiomatized.
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 TheoryIn 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.
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.
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.
∃x.¬p(x)
¬p(k) ∎ This result is not surprising given the dependence of Herbrand satisfaction on the vocabulary. Model TheoryModel theory in Herbrand logic is much simpler than it is in firstorder logic. Unlike firstorder 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: LoewenheimSkolemTarski does not hold in Herbrand logic.
Unlike Finite Herbrand Logic, not all theories are finitely axiomatizable. Theorem: Some Herbrand models are not finitely axiomatizable.
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.
© Copyright 2006 by
and the Stanford Logic Group
