The concept of evaluation for Herbrand Logic is the same as that for Relational Logic. Unfortunately, evaluation is usually not practical in this case for two reasons. First of all, truth assignments are infinite in size and so we cannot always write them down. Even when we can finitely characterize a truth assignment (e.g. when the set of true sentences is finite), we may not be able to evaluate quantified sentences mechanically in all cases. In the case of a universally quantified formula, we need to check all instances of the scope, and there are infinitely many possibilities. In the case of an existentially quantified sentence, we need to enumerate possibilities until we find one that succeeds, and we may never find one if the existentially quantified sentence is false.
Satisfaction has similar difficulties. The truth tables for Herbrand Logic are infinitely large and so we cannot write out or check all possibilities.
The good news is that, even though evaluation and satisfaction are not directly computable, there are effective procedures for indirectly determining validity, contingency, unsatisfiability, logical entailment, and so forth that work in many cases even when our usual direct methods fail. The key is symbolic manipulation of various sorts, e.g. the generation of proofs, which we describe in the next few chapters. But, first, in order to gain some intuitions about the power of Herbrand Logic, we look at some examples.
Use the arrow keys to navigate. Press the escape key to toggle all / one.