Notation for Model-Relation of formulae with free variables

Question

Lets assume we have a formula $\mathsf{path}(x,y)$ with free variables $x,y$, and $\mathsf{acyclic}$ with no free variables on the signature $\tau = \{E\}$ (i.e. Graphs). Informally, what the formula $\mathsf{path}$ does is check whether there is a path in-between $x$ and $y$, and $\mathsf{acyclic}$ checks whether the graph is acyclic.

More formally, a formula does not "check anything" but a graph is either a model of a formula or not. Hence,

$$ G \textrm{ is acyclic} \Leftrightarrow G \models \mathsf{acyclic}.$$

For the parameterized formula the case is a little bit more complicated since we have to assign a value from the universe of $G$ to $x$ and $y$. Lets assume $V(G)$ contains the nodes $v$ and $w$. We can define a function $\beta : \{x,y\} \to V(G)$ with

$$ \beta (a) := \begin{cases} v &\text{if } a=x,\\ w &\text{if } a=y. \end{cases} $$

Then we can write

$$ \textrm{ There is a $v,w$-path in } G \Leftrightarrow (G,\beta) \models \mathsf{path}.$$

This works, but it is a really bloated notation. I am using constructs like this a lot and I am trying to find a simpler notion. Simply writing $(G,v,w) \models \mathsf{path}$ is easy to understand in this context but it since there is no unique ordering of the free variables in $\mathsf{path}$ this not really nice, or is it?

Any ideas?

Answer 1

Okay, I found a notion like that with $[]$-brackets:

We write

$$ \textrm{ There is a $v,w$-path in } G \Leftrightarrow G \models\mathsf{path}[v,w] $$

where we substitute $x \leftarrow v$ and $y \leftarrow w$ (thus, in the order of the parameters).

Moreover we write for example

$$ \mathsf{path}[v,y] = \{ y \in V \mid \textrm{ There is a $v,y$-path > in } G \}.$$

The notion is based on the ordering of the parameters and the distinct between symbols in the formula ($x,y...$) and symbols in the graph ($v,w...$).