So this is a bit of a tangent, but your Santa Claus example really clarified something I've been reading about recently. I'm reading Lloyd's "Foundations of Log

So this is a bit of a tangent, but your Santa Claus example really clarified something I've been reading about recently. I'm reading Lloyd's "Foundations of Logic Programming", which essentially explains the fundamentals behind logic languages like Prolog. We write programs using uninterpreted functions[0] to represent our data, and define predicates to drive the program. The idea of using the Herbrand universe is that it gives a convenient universal starting point: if the program has a model in some universe, it will have a model in the Herbrand universe, and if the program does not have a model, it cannot have a model in the Herbrand universe. Your Santa Claus example helped me understand why the Herbrand universe is only useful if you restrict yourself to clauses (disjunctions under universal quantification). The Herbrand universe consists of all objects one has named (and objects one can form with function symbols, but we have none of those here), so it must necessarily falsify "~E x. x = Santa Claus". It's easy to find a model where this statement is true (take the empty universe, or the universe which contains only the Tooth Fairy), but there is no model of this statement in the Herbrand universe. [0] https://en.wikipedia.org/wiki/Uninterpreted_function https://en.wikipedia.org/wiki/Uninterpreted_function