Herbrand Logic -- First-order Syntax and Herbrand Semantics

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.

Syntax

The syntax of Herbrand logic is exactly the same as for first-order logic.

Definition (Vocabulary): A vocabulary V consists of:

A set of relation constants {r₁, ..., r_n}, each with an associated arity.
A set of function constants {f₁, ..., f_m}, each with an associated arity.
A non-empty set of object constants {c₁, ..., c_k}.
A set of variables {x₁,x₂,...}.

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:

A variable.
An object constant.
A function constant with arity n applied to n terms.
Only expressions produced by the above rules are terms.

Definition (Sentence): A sentence in V:

A relation constant with arity n applied to n terms.
(¬ φ) where φ is a sentence.
(φ ∨ ψ), where φ and ψ are sentences.
(φ ∧ ψ), where φ and ψ are sentences.
(φ ⇐ ψ), where φ and ψ are sentences.
(φ ⇒ ψ), where φ and ψ are sentences.
(φ ⇔ ψ), where φ and ψ are sentences.
(∀x.φ), where φ is a sentence.
(∃x.φ), where φ is a sentence.
Only expressions produced by the above rules are sentences.

An atom is a sentence of the form p(t₁,...,t_n). 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 Semantics

Herbrand 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.

|=_M s=t if and only if s and t are syntactically identical.
|=_M p(t₁,...,t_n) if and only if p(t₁,...,t_n) ∈ M.
|=_M ¬ ψ if and only if |#_M ψ.
|=_M φ ∧ ψ if and only if |=_M φ and |=_M ψ.
|=_M φ ∨ ψ if and only if |=_M φ or |=_M ψ.
|=_M φ ⇒ ψ if and only if |#_M φ or |=_M ψ.
|=_M φ ⇐ ψ if and only if |=_M ψ ⇒ φ.
|=_M φ ⇔ ψ if and only if either |=_M φ∧ψ or |=_M ¬φ ∧ ¬ψ.
|=_M ∀x.φ(x) if and only if |=_M φ(t) for all ground terms t in V.
|=_M ∃x.φ(x) if and only if |=_M φ(t) for some ground term t in V.

An open sentence φ(x₁,...,x_n) is satisfied by M if and only if ∀x₁...x_n.φ(x₁,...,x_n) is satisfied by M.∎

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 φ.

Δ |= φ wrt V if and only if |=_M Δ implies |=_M φ, where M is a Herbrand model for V

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 Semantics

To 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

|M|: universe
For each n-ary relation constant p an n-ary relation p^M over |M|
For each n-ary function constant f an n-ary function f^M over |M|
For each object constant c an element c^M from |M|

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(e_v): Let v be a variable assignment and M a first-order model. e_v maps a term to an element of |M|.

For variable x, e_v(x) = v(x)
For object constant c, e_v(c) = c^M
For terms t₁,...,t_n, e_v(f(t₁,...,t_n)) = f^M(e_v(t₁),...,e_v(t_n))

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.

|=_M t₁=t₂[v] iff e_v(t₁)=e_v(t₂)
|=_M p(t₁,...,t_n)[v] iff <e_v(t₁),...,e_v(t_n)> ∈ p^M
|=_M ¬ φ[v] iff |# φ[v]
|=_M φ ∧ ψ [v] iff |=_M φ[v] and |=_M ψ[v]
|=_M φ ∨ ψ [v] iff |=_M φ[v] or |=_M ψ[v]
|=_M φ ⇒ ψ [v] iff |#_M φ[v] or |=_M ψ[v]
|=_M φ ⇐ ψ [v] iff |=_M ψ ⇒ φ [v]
|=_M φ ⇔ ψ [v] iff |=_M φ ∧ ψ [v] or |=_M ¬φ ∧ ¬ψ [v]
|=_M ∀x.φ[v] iff for every d in |M| |=_M φ[v(x/d)]
|=_M ∃x.φ[v] iff for some d in |M| |=_M φ[v(x/d)]

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.

Δ |= φ if and only if for all variable assignments v and u, |=_M Δ[v] implies |=_M φ[u], where M is a first-order model

Examples

The following sentence has two satisfying Herbrand models for the vocabulary {p, a, b}. It has infinitely many first-order models.

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}.

However, in first-order logic, regardless the vocabulary, they are always satisfiable, e.g. {{1,2}, p={<1>}, a=1}. In Herbrand logic, enlarging the vocabulary to include an extra element is sufficient for satisfiability in this example: the vocabulary {p, a, b} allows the satisfying model {p(a)}.

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.

This set of sentences is satisfied by the model {p(a), ¬p(b)} for vocabulary {p, a, b}. But, if we were to drop out the ¬ p(b) sentence, under the new definition of satisfaction, the vocabulary would be {p, a}, which as commented above is unsatisfiable. That is, under this new definition of satisfaction, a set of sentences could be satisfiable, but a subset of those sentences could be unsatisfiable. Clearly, that would cause havoc in proof procedures; by fixing the vocabulary up front, in this case to {p, a, b}, the satisfiability of a set of sentences ensures the satisfiability of every subset.