Is the "ancestor" relationship impossible to define in first-order logic?

1k Views Asked by At

Definition: Given a binary relationship $R$, an ancestor relationship $R^*$ exists between $a$ and $b$ iff there is a chain of relationships $R$ connecting $a$ and $b$, for example, $Rax$, $Rxy$ and $Ryb$.

$R^*$ is trivial to define in logic programming (whose logical aspect is often said to be a subset of first-order logic). However, a paper I was reading claimed that $R^*$ cannot be defined in first-order logic. Is this true?


A Prolog definition of ancestor given parent:

$$ \begin{align} ancestor(X, Y) & \leftarrow parent(X, Y) \\ ancestor(X, Y) & \leftarrow parent(X, Z) \land ancestor(Z, Y) \end{align} $$

2

There are 2 best solutions below

1
On BEST ANSWER

The main reason is that First-Order Logic uses Tarskian semantics and logic programming uses Herbrand semantics. This has various consequences when it comes to expressiveness and other properties like compactness and completeness. For more details, see for example The Herbrand Manifesto or Herbrand Semantics, where your example (transitive closure) is discussed.

7
On

Yes, this is a standard application of the compactness theorem.

Here's a rough idea. Consider a theory which says (and adopt a mild abuse of notation):

  • $aR^*b$,

  • There is no $c_1$ with $aRc_1Rb$,

  • There are no $c_1,c_2$ with $aRc_1Rc_2Rb$,

  • There are no $c_1,c_2,c_3$ with $aRc_1Rc_2Rc_3Rb$,

  • etc.

This is obviously finitely consistent (just consider a "chain of length $n$" for $n$ large enough), but equally obviously unsatisfiable. So by compactness some clause must not actually be first-order expressible - and the only option is the first one.


EDIT: Re: the prolog definition you describe (caution: I'm not familiar with prolog); at a quick glance "negation-as-failure" is a bit nuanced. I would start by observing that first-order logic does not allow recursive, or least-fixed-point, definitions; in particular, the transitive closure of a definable relation in a structure need not be definable in that same structure.

  • Wait, but isn't Godel coding all about recursive definitions? Well, sort of - but there's some subtleties there. Godel shows that in certain structures/theories we can handle certain recursive constructions in a "reasonably decent" way. That's a far cry from what's wanted here.

As I said above, at a glance "negation-as-failure" has some subtlety to it (specifically, nonmonotonicity). However I do think that the above is really the heart of the issue, and will wind up being relevant to however one tries to link prolog and first-order logic.