## Herbrand SemanticsMichael GeneserethTimothy Hinrichs?? Eric Kao
## 1. IntroductionThe traditional semantics for First Order Logic (sometimes called Tarskian semantics) is based on the notion of interpretations. An interpretation consists of an arbitrary set of objects (called the universe of discourse) and an interpretation function (1) that maps object constants into elements of this set, (2) that maps function constants into functions on this set, and (3) that maps relation constants into relations on this set. Herbrand semantics is an alternative semantics for First Order Logic based directly on truth assignments for ground sentences rather than interpretations. A model is simply a truth assignment for the ground atoms our language. (Equivalently, it is an arbitrary subset of the ground atoms in our language.) In Herbrand semantics, there is no external universe and no interpretation function for constants. In effect, all ground terms are treated as opaque - they "represent" themselves. Herbrand semantics is widely used in computational settings, notably in database systems, logic programming, and answer set programming. And it has begun to supplant Tarskian semantics in introductory courses in Logic. One important advantage of Herbrand semantics is simplicity. It is conceptually simpler than Tarskian semantics; and, consequently, it is easier to teach and to learn. To see this, consider the meaning of quantifiers and variables under the two different semantics. In Tarskian semantics, the meaning of quantifiers is based on the notion of variable assignments and versions of variable assigments. A variable assignment is an assignment of variables to objects in the universe of discourse associated with an interpretation. A version of a variable assignment is a variable assignment in which one of the variables is mapped to a possibly different object in the universe of discourse. A universally quantified sentence is said to be true for a given interpretation and variable assignment if and only if it is true for every variation of the given variable assignment. It is a mouthful to say and even harder for people to understand. In Herbrand semantics, the meaning of quantifiers is much simpler. A universally quantified sentence is true if and only if all of the instances of the quantified sentence are true. An existentially quantified sentence is true if and only if there is some instance that is true. That is all. There are no interpretations and no variable assignments and no variations of variable assignments. Moreover, our common intuitions about quantifiers are respected. In Herbrand semantics, if a sentence phi(tau) holds for every ground term tau, then the sentence Ax.phi(x) is true. In other words, a universally quantified sentence is logically equivalent to the set of instances of its scope. (This property does not hold in Tarskian semantics.) A second important feature of Herbrand semantics is expressiveness. While it is not possible to finitely axiomatize integer arithmetic with Tarskian semantics, this can be done with Herbrand Semantics. While it is not possible to formalize transitive closure in first-order logic with Tarskian semantics, this can be be done with Herbrand semantics without introducing negation as failure or model minimization. The downside of Herbrand semantics is a loss of some logical properties possessed by Tarskian semantics. However, as we shall argue, Herbrand semantics preserves the properties that really matter. First of all, Herbrand Logic is not compact - there are infinite sets of sentences that are inconsistent while every finite subset is consistent. The upshot of this is that there are infinite sets of sentences where we cannot demonstrate unsatisfiability with a finite argument within the language itself. Fortunately, this does not cause any practical difficulties, since in all cases of practical interest we are working with finite sets of premises. Another deficiency of Herbrand semantics vis a vis Tarksian semantics is that with Herbrand semantics there are restrictions on the cardinality of the worlds that can be axiomatized. Since there is no external universe, the cardinality of the structures that can be axiomatized is equal to the number of ground terms in the language. (To make things easy, we can always choose a countable language. We can even choose an uncountable language, though doing so would ruin some of the nice properties of Herbrand semantics. On the positive side, it is worth noting that in many practical applications we do not care about uncountable sets. Although there are uncountably many real numbers, remember that there are only countably many floating point numbers.) More significantly, recall that the Lowenheim-Skolem Theorem assures us that even with Tarskian semantics we cannot write sentences that distinguish models of different infinite cardinalities. So, it is unclear whether this restriction has any practical significance. Herbrand Logic shares most important properties with Tarskian Logic. The deductive calculus is complete for all finite axiomatizations. In the absence of function constants, the calculus derives the exact same set of sentences. When we add functions, we lose this nice property. However, we get some interesting benefits in return. For one, it is possible in Herbrand Logic (with functions) to finitely axiomatize arithmetic. As we know from Godel, this is not possible in a first-order language with Tarskian semantics. The downside is that we lose completeness. However, it is nice to know that we can at least define things, even though we cannot prove them. Moreover, as mentioned above, we do not actually lose any consequences that we are able to deduce with First-Order Logic. Note that Herbrand semantics is not new here. It is widely used in discussions of automated reasoning and logic programming and databases. However, in most cases, it is treated (justifiably) as a special case of first-order semantics. In this paper, we turn things around - we start with Herbrand semantics, we study its logical and computational properties, and we then talk about how it can be extended to First Order Logic. We begin the paper with a definition of the syntax of First Order Logic. We then introduce Herbrand semantics. We discuss its expressiveness and equivalence of various subsets to other logics. We then discuss its proof theory. Finally, we talk about the relationship between Herbrand semantics and Tarskian semantics. ## 2. SyntaxIn Propositional Logic, sentences are constructed from a basic vocabulary of propositional constants. In Herbrand Logic, there are no propositional constants; instead we have In our examples here, we write both variables and constants as strings of letters, digits, and a few non-alphanumeric characters (e.g. "_"). By convention, variables begin with letters from the end of the alphabet (viz. Note that there is no distinction in spelling between object constants, function constants, and relation constants. The type of each such word is determined by its usage or, in some cases, in an explicit specification. As we shall see, function constants and relation constants are used in forming complex expressions by combining them with an appropriate number of arguments. Accordingly, each function constant and relation constant has an associated A A A Note that functional expressions can be nested within other functional expressions. For example, if There are three types of A q(a, y)
A x.(p(x) ⇒ q(x,x)))
An x.(p(x) ∧ q(x,x)))
Note that quantified sentences can be nested within other sentences. For example, in the first sentence below, we have quantified sentences inside of a disjunction. In the second sentence, we have a quantified sentence nested inside of another quantified sentence. x.p(x)) ∨ (∃x.q(x,x))(∀ x.(∃y.q(x,y)))
As with Propositional Logic, we can drop unneeded parentheses in Herbrand Logic, relying on precedence to disambiguate the structure of unparenthesized sentences. In Herbrand Logic, the precedence relations of the logical operators are the same as in Propositional Logic, and quantifiers have higher precedence than logical operators. The following examples show how to parenthesize sentences with both quantifiers and logical operators. The sentences on the right are partially parenthesized versions of the sentences on the left. (To be fully parenthesized, we would need to add parentheses around each of the sentences as a whole.)
Notice that, in each of these examples, the quantifier does
An expression in Herbrand Logic is An occurrence of a variable is x.q(x,y)
A sentence is p(y) ⇒ ∃x.q(x,y)∀ y.(p(y) ⇒ ∃x.q(x,y))
## 3. Herband SemanticsThe For a vocabulary with object constants p(a), p(b), q(a,a), q(a,b), q(b,a), q(b,b)}
It is worthwhile to note that, for a given relation constant and a finite set of terms, there is an upper bound on the number of ground relational sentences that can be formed using that relation constant. In particular, for a set of terms of size n-tuples of object constants; and hence there are b ground relational sentences for each ^{n}n-ary relation constant. Since the number of relation constants in a vocabulary is finite, this means that the Herbrand base is also finite.Of course, not all Herbrand bases are finite. In the presence of function constants, the number of ground terms is infinite; and so the Herbrand base is infinite. For example, in a language with a single object constant p(a), p(f(a)), p(f(f(a))), ...}
A
As with Propositional Logic, once we have a truth assignment for the ground relational sentences of a language, the semantics of our operators prescribes a unique extension of that assignment to the complex sentences of the language. The rules for logical sentences in Herbrand Logic are the same as those for logical sentences in Propositional Logic. A truth assignment In order to define satisfaction of quantified sentences, we need the notion of instances. An A universally quantified sentence is true for a truth assignment if and only if As an example of these definitions, consider the sentence ∀
We know that Now let's consider a case with nested quantifiers. Is ∀
To determine the truth of the first of these existential sentences, we must find at least one instance of the scope that is true. The possibilities are shown below. Of these, the first is true; and so the first existential sentence is true.
Now, we do the same for the second existentially quantified. The possible instances follow. Of these, again the first is true; and so the second existential sentence is true.
Since both existential sentences are true, the original universally quantified sentence must be true as well. A truth assignment ## 4. Example - Modular ArithmeticIn this example, we show how to characterize Modular Arithmetic in Herbrand Logic. In Modular Arithmetic, there are only finitely many objects. For example, in Modular Arithmetic with modulus 4, we would have just four integers - 0, 1, 2, 3 - and that's all. Our goal here to define the addition relation. Admittedly, this is a modest goal; but, once we see how to do this; we can use the same approach to define other arithmetic relations. Let's start with the
Now, let's axiomatize the
Properly, we should write out the negative literals as well. However, we can save that work by writing a single axiom asserting that x.∀y.∀z.(next(x,y) ∧ next(x,z) ⇒ same(y,z)In order to see why this saves us the work of writing out the negative literals, we can write this axiom in the equivalent form shown below. x.∀y.∀z.(next(x,y) ∧ ¬same(y,z) ⇒ ¬next(x,z))The addition table for Modular Arithmetic is the usual addition table for arbitrary numbers except that we wrap around whenever we get past 3. For such a small arithmetic, it is easy to write out the ground relational sentences for addition, as shown below.
As with x.∀y.∀z.∀w.(plus(x,y,z) ∧ ¬same(z,w) ⇒ ¬plus(x,y,w))
That's one way to do things, but we can do better. Rather than writing out all of those relational sentences, we can use Herbrand Logic to define
One advantage of doing things this way is economy. With these sentences, we do not need the ground relational sentences about ## 5. Example - Peano ArithmeticNow, let's look at the problem of encoding arithmetic for all of the natural numbers. Since there are infinitely many natural numbers, we need infinitely many terms. One way to get infinitely many terms is to have a vocabulary with infinitely many object constants. While there is nothing wrong with this in principle, it makes the job of axiomatizing arithmetic effectively impossible, as we would have to write out infinitely many literals to capture our successor relation. An alternative approach is to represent numbers using a single object constant (e.g. 0) and a single unary function constant (e.g. Unfortunately, even with this representation, axiomatizing Peano Arithmetic is more challenging than axiomatizing Modular Arithmetic. We cannot just write out ground relational sentences to characterize our relations, because there are infinitely many cases to consider. For Peano Arithmetic, we must rely on logical sentences and quantified sentences, not just because they are more economical but because they are the only way we can characterize our relations in finite space. Let's look at the same relation first. The axioms shown here define the
It is easy to see that these axioms completely characterize the Once we have the
The axiomatization of multiplication is analogous. Multiplying any number by 0 produces 0. If a number
That's all we need - just three axioms for Before we leave our discussion of Peano aritmetic, it is worthwhile to look at the concept of Diophantine equations. A x^{2} + 2y = 4z
A Diophantine equations can be readily expressed as sentences In Peano Arithmetic. For example, we can represent the Diophantine equation above with the sentence shown below. x.∀y.∀z.∀u.∀v.∀w.(times(x,x,u) ∧ times(2,y,v) ∧ plus(u,v,w) ⇒ times(4,z,w))
This is a little messy, but it is doable. And we can always clean things up by adding a little syntactic sugar to our notation to make it look like traditional math notation. Once this mapping is done, we can use the tools of logic to work with these sentences. In some cases, we can find solutions; and, in some cases, we can prove that solutions do not exist. This has practical value in some situations, but it also has significant theoretical value in establishing important properties of Herbrand Logic, a topic that we discuss in a later section. ## 5. Logical PropertiesRecall that compactness means that, if an infinite set of sentences is unsatisfiable, there is some finite subset that is unsatisfiable. It guarantees finite proofs. Theorem 5 (NonCompactness). : Herbrand logic is not compact. Proof. Consider the following infinite set of sentences.
Assuming the vocabulary is {p, a, f }, the ground terms are a, f (a), f (f (a)), . . . , and this set of sentences entails ∀x.p(x). Add in the sentence ∃x.¬p(x). Clearly, the infinite set is unsatisfiable. However, every finite subset is satisfiable with respect to the vocabulary {p,a,f}. (Every finite subset is missing either ∃x.¬p(x) or one of the sentences above. If it is the former, the set is satisfiable, and if it is the latter, the set can be satisfied by making the missing sentence false.) Thus, compactness does not hold. 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[∆]. The set of sentences entailed by a set of sentences ∆ is denoted Cn[∆]. Also, the set of sentences true in all models in the set M is denoted as usual by Th[M]. Theorem 7. : 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 8. : Lowenheim-Skolem-Tarski does not hold in Herbrand logic. Proof. Lowenheim-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 8. : 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. 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 usual effect in Herbrand logic. Theorem 6. In Herbrand logic, Skolemization does not preserve satisfiability. Proof. The following set of sentences are unsatisfiable. p(a) ∃x.¬p(x) Skolemizing produces a satisfiable set of sentences: p(a), ¬p(k) This result is not surprising given the dependence of Herbrand satisfaction on the vocabulary. ## 6. Proof TheoryCorollary 7 (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). ## n. Herbrand Logic Versus First Order LogicNow that we have presented the semantics and proof systems for both First Order Logic and Herbrand Logic, we can talk about deciding which logic to use in a given situation. We start by comparing the two logics with respect to several theoretical properties. For any given set of equality-free sentences Σ, we know that every satisfying truth assignment in Herbrand Logic corresponds to a satisfying First Order Logic interpretation of Σ. As a result, if an equality-free sentence φ is satisfied in all of the First Order Logic interpretations that satisfy Σ, then φ is also satisfied in all the Herbrand Logic truth assignments of Σ. From the definition of logical entailment, we obtain the following theorem that whenever a sentence is entailed under First Order Logic, it is also entailed under Herbrand Logic. That is, Herbrand Logic is deductively more powerful than First Order Logic. Theorem 10.3: Given a set of equality-free sentences Σ and an equality-free sentence φ, if Σ |= A similar result holds for sentences with equality when we extend Herbrand Logic to incorporate equality. We also know that the same set of sentences conveys more information in Herbrand Logic than in First Order Logic in the sense that the set of sentences admits fewer satisfying worlds and entails more conclusions. However, in a given situation, which logic should we use? In general, we should use the logic that allows us to simply and accurately model the information available. In the case that the set of objects is known and fixed in advance, Herbrand Logic is the natural choice because it is simple and accurate in modeling the information. In many applications, the exactly set of objects is not fixed, but a "covering" set of identifiers can be used instead. For example, United States presidents is not fixed, but we can fix the Herbrand universe {a, s(a), s(s(a)), ...} to stand for all actual and potential presidents. For another example, new English essays are written everyday, but we can fix a Herbrand universe to stand for all existing and potential English essays. Herbrand Logic continues to make sense in these situations because of its simplicity and deductive power. Finally, there are cases when not even a covering set of identifiers can be fixed in advance. For example, consider the class of all arithmetic structures where the plus operator is commutative. In this class the size of the underlying set of objects can be arbitrarily large, exceeding any fixed set of identifiers (even an infinite set of identifiers). In these cases, Herbrand Logic is inappropriate because it cannot accurately model the information available. First Order Logic, which imposes no restrictions on the set of objects, is the more appropriate choice. We stated in section 10.12 that First Order Fitch is sound and complete for First Order Logic. In Herbrand Logic, we have the analogous soundness theorem but not the completeness theorem. Theorem 10.4 (Soundness of Herbrand Fitch): Given a set of sentences Σ and a sentence φ, if Σ |- Theorem 10.5 (Incompleteness of Herbrand Fitch): There exists a set of sentences Σ and a sentence φ such that Σ |= The upshot is that Herbrand Logic itself is expressively powerful but the proof system for Herbrand Logic is not as powerful as its semantics. Even so, the proof system for Herbrand Logic remains more powerful than the proof system for First Order Logic. Theorem 10.6: Given a set of equality-free sentences Σ and an equality-free sentence φ, if Σ |- A similar result holds for sentences with equality when we include the two equality rules into Fitch for Herbrand Logic. |