I am learning a course from Stanford University, and it introduces the notion of Herbrand Logic. However in Wikipedia I cannot find a definition specifically for "Herbrand Logic", only for Herbrand Base or Herbrand Theorem, concepts that also exist in relational logic / predicate logic ?


The Stanford Introduction to Logic course offers the following difference between Relational Logic and Herbrand Logic in the Recap of Chapter 9:

Herbrand Logic is an extended version of Relational Logic that includes functional expressions. Since functional expressions can be composed with each other in infinitely many ways, the Herbrand base for Herbrand Logic is infinite, allowing us to axiomatize infinite relations with a finite vocabulary. Other than the addition of functional expressions, the syntax and semantics of Herbrand Logic is the same as that of Relational Logic.

According to Francois Bry, Mike Genesereth, Tim Hinrichs, and Nat Love

Herbrand Logic = First-order syntax + Herbrand semantics

They argue for this Herbrand Logic over First Order Logic for the following reason showing the difference between the two:

FOL was certainly not designed to model or manipulate finite machines, the central activities in computer science. More than that, at times it is ill-suited for the purpose. Consider a detailed model of a computer which shows how its state, e.g. memory contents and program counter, changes over time. Because time in a computer is discrete, state can only change on each clock tick. A finite memory modeled for countably many time steps would require a model of countably infinite size. But in first-order logic, there is no way to constrain such a model to one of countable size; if a set of first-order sentences has a model of infinite size, it has a model of every infinite size (Loewenheim-Skolem-Tarski). Thus, in first-order logic, the query, "is the program counter positive at every time step?" is not even expressible.

In summary, Relational Logic permits only a finite model; Herbrand Logic allows a countably infinite model and First Order Logic allows for an uncountably infinite model.

Francois Bry, Mike Genesereth, Tim Hinrichs, Nat Love. Herbrand Logic. Stanford Logic Group. Retrieved on September 2, 2019 at https://www.cs.uic.edu/~hinrichs/herbrand/html/index.html

Stanford Introduction to Logic. Retrieved on September 2, 2019 at http://intrologic.stanford.edu/notes/chapter_09.html

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.