First order logic Prolog anonymous variables

Question

The Prolog rule below:

grandparent(X,Z) :- parent(X,Y) , parent(Y,Z)

In first order logic is going to be:

∀x ∀y ∀z ((P (x, y) ∧ P (y, z)) → G(x, z))

In theory if we have an anonymous variable in our Prolog rule something like:

grandparent(X,Z) :- parent(X,Y, _ ) , parent(Y,Z, _ )

Lets say it is a surname, how can we present it in first order logic?

Answer 1

Simply use the rule:

"Give the child a name"

Note that the underscore is not a single variable. Two underscores in Prolog have nothing to do with each other.

We can simply replace the code with:

grandparent(X,Z) :-
    parent(X,Y,A),
    parent(Y,Z,B).

And now a logical "equivalent" would be:

∀x ∀y ∀z ∀a ∀b: ((P (x, y, a) ∧ P (y, z, b)) → G(x, z))

Note however that the two are not equivalent: since theoretically speaking (probably not here), the first parent/3 call, might have side effects, ground terms further, etc. Only a subset of Prolog maps to such logical constructs.