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


Frank Hubeny's answer is quite good, but let me add to it re: Herbrand semantics. In particular, I'm going to push back against the argument pro Herbrand logic cited in that answer.

It is true that Herbrand semantics permits only countable structures*, but that's not the full story: since first-order logic has the downwards Lowenheim-Skolem property, if Herbrand semantics permitted exactly the countable structures then on the level of entailment between (sets of) sentences Herbrand logic and first-order logic would coincide. However, the restriction in Herbrand semantics is stricter than that: roughly speaking, we only look at term structures.

This restriction results in some rather odd properties. Most importantly in my opinion is the complexity of the set of validities according to Herbrand semantics: namely, it has Turing degree 0^{omega}, which is extremely complicated. As a consequence, while first-order logic has a proof system which is sound, complete, and computably enumerable, there is no proof system for Herbrand logic which is sound, complete, and even arithmetically definable (the c.e. sets are very low in the arithmetical hierarchy). Similarly, Herbrand logic is not compact.

This is the "negative" aspect of the difference between first-order and Herbrand logic which Bry/Genesereth/Hinrichs/Love approach "positively," and an instance of a more general phenomenon: a gain in logical strength is generally accompanied by a loss in logical tameness, and so a stronger logic is not necessarily more desirable. See also the beginning and end of this old answer of mine.

One famous example of this is Lindstrom's theorem that there is no logic which is strictly stronger than first-order logic and has both the compactness and Lowenheim-Skolem properties. **

*Actually it's not quite true - it's only true for countable (or finite) languages. If L is an uncountable language, Herbrand semantics permits models of cardinality up to that of L. However, uncountable languages aren't really in the spirit of Herbrand logic.

**There's an interesting shift in perspective here: although initially considered undesirable, the general stance - at least on the mathematical side of logic - is that the downwards Lowenheim-Skolem property is a good thing to have.


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.