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.
Articles by others on the same topic
There are currently no matching articles.