Herbrand Logic
| |||||
This page defines the syntax and semantics of Herbrand logic, and for the purpose of comparison, first-order logic. It finishes with a couple of quick examples illustrating the difference between first-order semantics and Herbrand semantics.
SyntaxThe syntax of Herbrand logic is exactly the same as for first-order logic. Definition (Vocabulary): A vocabulary V consists of:
For the sake of simplicity, we assume the set of constants in a vocabulary is finite. A countable set of constants changes the wording of certain theorems, but conceptually nothing changes. Definition (Term): A term in V:
Definition (Sentence): A sentence in V:
An atom is a sentence of the form p(t1,...,tn). A literal is either an atom or the negation of an atom. A ground sentence has no variables or quantifiers. A closed sentence has no free variables, whereas an open sentence does have free variables. We treat free variables in an open sentence as being implicitly universally quantified. Herbrand SemanticsHerbrand logic differs from first-order logic solely in the structures it considers to be models. The semantics of a given set of sentences is defined to be the set of Herbrand models that satisfy it, for a given vocabulary. Definition (Herbrand Model): A Herbrand model for vocabulary V is any set of ground atoms in V. Definition (Herbrand Satisfaction): Let φ be a closed sentence and M a Herbrand model in the vocabulary V.
We always assume that satisfaction for a set of sentences Δ is defined with respect to a vocabulary that includes all the constants and variables that appear in Δ. Otherwise, a model might satisfy neither a sentence nor its negation. One of the consequences of this definition is that the theory of equality is fixed in Herbrand logic: every ground term is distinct from every other ground term and the universe. Another consequence is that quantifiers range over exactly the set of all ground terms. That is, Herbrand logic builds in a domain closure axiom (which is sometimes infinitely long) and unique-names axioms. Definition (Herbrand Entailment): Let Δ be a set of closed sentences and V a vocabulary that is a superset of the vocabulary of Δ. Let φ be a closed sentence. Δ entails φ with respect to vocabulary V if and only if every Herbrand model for V that satisfies Δ also satisfies φ. If no vocabulary is named in satisfaction or entailment, it is assumed the minimal vocabulary is used, i.e. the vocabulary that includes just the constants in the sentences given. First-order SemanticsTo demonstrate the simplicity of Herbrand semantics, here we give the standard semantics of first-order logic for comparison. To be clear, Herbrand logic does not have the following semantics; it has the semantics from the last section. Definition (First-order Model): A first-order model M consists of
Definition (Variable Assignment): In a model M, a variable assignment is a mapping of all the variables in the vocabulary to elements in |M|. Given an arbitrary model and a variable assignment for that model, every term in the language is assigned an element in that model's universe. Definition(ev): Let v be a variable assignment and M a first-order model. ev maps a term to an element of |M|.
Finally we can define satisfaction in a model. Satisfaction assumes there is some given variable assignment v. Definition(First-order Satisfaction): Let M be a model and v a variable assignment for M. |=M φ is defined as follows.
Definition (First-order Entailment): Let Δ be a set of sentences and φ be a sentence. Δ entails φ if and only if every first-order model that satisfies Δ[v] for all variable assignments v also satisfies φ[v] for all variable assignments v. ExamplesThe following sentence has two satisfying Herbrand models for the vocabulary {p, a, b}. It has infinitely many first-order models.
Herbrand Models: {p(a)}, {p(a), p(b)} Some First-order Models: {{1},p={<1>},a=1,b=1}, {{1,2,3,...},p={<17>,<63>}, a=17, b=51}, {Reals, p={<3.14159...>,<17.0>}, a=3.14159..., b=0.33333...} In Herbrand logic, restricting the vocabulary to {p, a} ensures there is only one satisfying model: {p(a)}. In first-order logic, shrinking the vocabulary does not reduce the number of models at all; the only difference is that models of the smaller vocabulary do not have an assignment for b. The following sentences are Herbrand unsatisfiable for the vocabulary {p, a}.
∃x.¬ p(x) More generally, in first-order logic, changing the vocabulary never changes the satisfiability (again the vocabulary must always be a superset of the symbols in the axiom set), whereas in Herbrand logic, changing the vocabulary can affect satisfiability. A note on the dependence of Herbrand satisfaction on a vocabulary. To see why satisfaction is defined as it is, suppose instead of fixing the vocabulary up front (which defines the class of candidate models), we instead define satisfaction so that the vocabulary is gleamed from the sentences we are given. Now consider the following axioms.
¬p(b) ∃x.¬p(x)
© Copyright 2006 by
and the Stanford Logic Group
|