Synopsis of Herbrand Logic

• Without functions, entailment is decidable.
• With functions, entailment is not semi-decidable and satisfiability is not semi-decidable.
• With functions, premises in the ∀* fragment, query in the ∃* fragment, entailment is semi-decidable.
• The theory of integer arithmetic, i.e. <N, <, +, *>, is finitely axiomatizable.
• Four very successful applications of logic in computer science, deductive databases, constraint satisfaction, logic programming, and formal verification, all make assumptions that are embodied in Herbrand logic: a domain closure axiom and unique names axioms.
• Inductive Theorem Proving is defined as theorem proving in Herbrand logic.

Another Logic?

Logic was invented in an attempt to understand the foundations of mathematics. What does it mean for a theorem to be true? Does x*y really equal y*x? Paradoxes are sentences that are neither true nor false, yet they creep into mathematics; is that bad, good, or is it irrelevant? How can we prove that a mathematical proof is correct? How do we even make sense of these questions?

First-order logic (FOL) is one answer to the last question. If some theorem of a mathematical system can be proven from the axioms of that system written in first-order logic, the theorem holds. Because of this commitment to mathematical truth in general, FOL was defined so that it can be used across a broad spectrum of mathematics. It is not tailored to the study of integers, real numbers, geometry, topology, or any particular branch of mathematics.

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.

Nevertheless logic is used throughout computer science, most notably in deductive database theory, constraint satisfaction, logic programming, and formal verification. Often, the foundations of these fields of study are taught as special cases of first-order logic. Here we depart from that practice (after having repeatedly taught first-order semantics only to see even the good students misunderstand the very notion of a model), and begin with a logic tailored for computer scientists, whose main interests are modeling and manipulating computers. We have employed the name Herbrand logic, to reflect its first-order syntax and Herbrand semantics.

Part of the motivation for building this website was the frustration brought about by looking for and failing to find general results on this logic. Herbrand semantics appears repeatedly in the literature of logic programming, but the only results we were able to find in that community are for the fragment of Herbrand logic that coincides with first-order logic, i.e. ∀* premises and ∃* queries. After constructing the site, we realized that all the results here have been well known in the inductive theorem proving (ITP) community, where the central concern turns out to be proving theorems in Herbrand logic. The nonmonotonic community has also studied this logic in at least two forms, both of which fall under the umbrella of minimal entailment: Domain Circumscription and Herbrand entailment.

Our aims are slightly different than the aims of researchers in the ITP and Nonmon communities. We are looking for ways to unify the work on deductive databases, constraint satisfaction, logic programming, and formal verification so that systems given problems stated in Herbrand logic can employ the results from these four areas to efficiently solve those problems. On this site, we have attempted to explain some of Herbrand Logic's model theory and proof theory without slanting analysis toward one application or another. By treating it as a logic in its own right, we hope to achieve two goals: (1) provide a simple framework for building machines that can efficiently reason throughout the space of Herbrand logic and (2) improve how logic is taught to computer scientists.

Reading Guide

• Syntax and Semantics: Definitions for the syntax and semantics of Herbrand logic, along with syntax and semantics of first-order logic, for comparison.
• Proof and Model Theory: Some (un)decidability results for entailment and some finite axiomatizability results.
• Goedel: A discussion of Goedel's incompleteness proof and results showing how to finitely encode integer arithmetic in Herbrand logic.
• Applications: Definitions for deductive databases, constraint satisfaction problems, a couple of logic programming languages, and formal verification, all rooted in Herbrand logic.

On Symbology

Contributors, alphabetically