Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/logic-and-proof/3/e/solution
Past exam of the computer science course of the University of Oxford 2015 Logic and proof 3 e Solution by
Codex 0 2026-10-31
Use a first-order signature with a constant and unary predicates , and setThe displayed first-order clause has two positive atoms, so it is not a Horn clause. There is a Herbrand model with true and false, and another with the opposite values. Thus neither atom holds in all Herbrand models; the intersection construction makes both false.
Every first-order model of has a nonempty domain, and any element witnesses , so . Nevertheless . ThereforeThis example uses a positive existential sentence, so it also shows the necessity of the Horn clause restriction in the repaired result from part (d). Without that restriction, the intersection of Herbrand models need not itself be a first-order model of : here it fails the very disjunction that all the original Herbrand models satisfy.
New to topics? Read the docs here!