Tarskian semantics and Herbrand semantics are two ways of assigning meaning to first-order logic. They agree on the general aim: to explain when formulas are true, when a theory has a model, and when one statement follows from another. But they differ in how freely the language may be interpreted.
In Tarskian semantics, a logical language is interpreted inside a structure. The structure provides a domain of objects, and it assigns meanings to the non-logical symbols of the language. Constants denote objects in the domain, function symbols denote actual functions on that domain, and predicate symbols denote relations over the domain.
This makes Tarskian semantics very general. The objects of the domain do not have to be linguistic objects or terms. They may be numbers, sets, people, points in space, algebraic objects, or anything else suitable for the intended interpretation. Truth is evaluated relative to such a structure and, often, relative to an assignment of values to variables.
For example, a formula is true in a structure if it is satisfied under the relevant interpretation of its symbols. A sentence is a logical consequence of a theory if it is true in every Tarskian model of that theory. Thus Tarskian semantics asks: what could these symbols mean in some mathematical structure?
Herbrand semantics is more syntactic. Instead of allowing arbitrary domains, it fixes the universe to be the set of ground terms that can be built from the constants and function symbols of the language. This is called the Herbrand universe.
In a Herbrand interpretation, constants and function symbols are interpreted as themselves. A constant denotes that very constant, and a compound term denotes that very compound term. The main remaining freedom is deciding which ground atoms are true. In this way, Herbrand semantics turns questions about models into questions about syntactic terms and atomic facts over those terms.
This makes Herbrand semantics especially important in automated theorem proving, resolution, and logic programming. It allows first-order reasoning to be connected to ground instances and syntactic search. Herbrand semantics asks: what follows when the terms of the language themselves are treated as the objects of discourse?
The difference can be put simply:
Tarskian semantics is model-theoretic and domain-general. It allows many possible domains and many possible interpretations of the non-logical symbols.
Herbrand semantics is term-based and syntactic. It fixes the domain to the ground terms generated by the language and interprets functions and constants canonically.
So Tarskian semantics emphasizes arbitrary mathematical structures, while Herbrand semantics emphasizes the internal term structure of the language itself.
The interpolation lemma, especially in the Craig interpolation tradition, says roughly that if a formula or sentence A entails another formula or sentence B, then there is an intermediate formula I, called an interpolant, such that:
A entails I,
I entails B,
and I uses only the non-logical symbols common to both A and B.
In Tarskian semantics, this is understood through truth in arbitrary structures. If every model of A is also a model of B, then there is a formula in the shared vocabulary that captures the semantic bridge between them. The interpolant expresses what A contributes toward B using only the language that both sides have in common.
The philosophical point is that if B follows from A, then whatever is responsible for that entailment can be stated without using symbols that occur only on one side. Tarskian interpolation is therefore a strong model-theoretic statement about consequence across all relevant structures.
In Herbrand semantics, interpolation takes on a more syntactic and proof-oriented character. Since the universe consists of ground terms, entailment is often analyzed by looking at ground instances, Herbrand models, or refutations of ground clause sets.
Here, an interpolant can often be extracted from a proof or refutation. It represents the part of the reasoning that is shared between two collections of formulas or clauses. As in the Tarskian case, the interpolant must use only symbols common to both sides. But the mechanism is usually more concrete: it is tied to ground terms, clauses, substitutions, and proof search.
This is why Herbrand-style interpolation is especially natural in automated reasoning. A refutation may reveal exactly which shared atoms, terms, or clauses are doing the work. The interpolant is then a compact expression of that shared content.
Tarskian semantics interprets first-order logic in arbitrary mathematical structures. Herbrand semantics interprets it over the syntactic universe of ground terms.
Tarskian interpolation says that semantic consequence across arbitrary structures factors through a formula in the shared vocabulary.
Herbrand interpolation says that, when reasoning is grounded in terms and ground instances, the shared part of a proof or refutation can be extracted as an interpolant over the shared vocabulary.
In short, Tarskian semantics gives the broad model-theoretic picture, while Herbrand semantics gives a syntactic, proof-oriented picture that is particularly useful for computation and automated reasoning.