Logical entailment for Herbrand Logic is defined the same as for Propositional Logic and Relational Logic. A set of premises logically entails a conclusion if and only if every truth assignment that satisfies the premises also satisfies the conclusions. In the case of Propositional Logic and Relational Logic, we can check logical entailment by examining a truth table for the language. With finitely many proposition constants, the truth table is large but finite. For Herbrand Logic, things are not so easy. It is possible to have Herbrand bases of infinite size; and, in such cases, truth assignments are infinitely large and there are infinitely many of them, making it impossible to check logical entailment using truth tables.
All is not lost. As with Propositional Logic and Relational Logic, we can establish logical entailment in Herbrand Logic by writing proofs. In fact, it is possible to show that, with a few simple restrictions, a set of premises logically entails a conclusions if and only if there is a finite proof of the conclusion from the premises, even when the Herbrand base is infinite. Moreover, it is possible to find such proofs in a finite time. That said, things are not perfect. If a set of sentences does not logically entail a conclusion, then the process of searching for a proof might go on forever. Moreover, if we remove the restrictions mentioned above, we lose the guarantee of finite proofs. Still, the relationship between logical entailment and finite provability, given those restrictions, is a very powerful result and has enormous practical benefits.
In this lesson, we talk about the non-compactness of Herbrand Logic and the loss of completeness in our proof procedure. In the next lesson, we look at an extension to Fitch, called Induction, that allows us to prove more results in Herbrand Logic.
Use the arrow keys to navigate. Press the escape key to toggle all / one.