I am not sure what Δ ⊨ Ǝx path(a,x) means (its not Prolog), but i am interpreting it as “there exists an x such that there is a path from a to x”. In this case you have path(a, X).

In Prolog (as in inductive proofs in math) you tend to write definitions in terms of themselves … can you see how this could look like when translated to two (or more) Prolog rules?

Edit:

Δ ⊨ Ǝx path(a,x)

I guess this literally means from delta (Δ) it is possible to semantically proof that there exists an x such that path(a,x) is true.

I guess Δ stands for the Prolog program that defines what a path is within the structure given.

But, i am wondering – does semantic proof (double turnstile) really apply to Prolog queries, or should it be a single turn stile (syntactic proof) – since in prolog one simply computes one example – one can also repeatendly show all x for which there is a path from a to x – but its also merely examples rather than a symbol proof.