Herbrand semantics: A truth semantics for computational logic

Semantics is what gives meaning to a logical language. Introductory books in formal logic almost invariably employ Tarskian semantics, a truth semantics that defines an interpretation as a variable assignment over a non-empty domain of discourse together with a signature interpretation. The problem with this semantics is that it generally dictates the undecidability of classical first-order logic due to an infinity of infinite models. In computational logic, decidability is a synonym for computability, and hence Tarskian semantics is not appropriate. In contrast, Herbrand semantics, also a truth semantics, provides us with finite, propositional-logic style, interpretations that guarantee decidability—even if at the price of fixed interpretations for first-order formulae or theories.