Notación para la relación de modelos de fórmulas con variables libres

Question

Supongamos que tenemos una fórmula $\mathsf{path}(x,y)$ con variables libres $x,y$ y $\mathsf{acyclic}$ sin variables libres en la firma $\tau = \{E\}$ (es decir, los gráficos). Informalmente, lo que la fórmula $\mathsf{path}$ es comprobar si hay un camino entre $x$ y $y$ y $\mathsf{acyclic}$ comprueba si el gráfico es acíclico.

Más formalmente, una fórmula no "comprueba nada", pero un gráfico es un modelo de una fórmula o no. Por lo tanto,

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

Para la fórmula parametrizada el caso es un poco más complicado ya que tenemos que asignar un valor del universo de $G$ a $x$ y $y$ . Supongamos que $V(G)$ contiene los nodos $v$ y $w$ . Podemos definir una función $\beta : \{x,y\} \to V(G)$ con

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

Entonces podemos escribir

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

Esto funciona, pero es una notación realmente hinchada. Estoy usando construcciones como esta un montón y estoy tratando de encontrar una noción más simple. Simplemente escribiendo $(G,v,w) \models \mathsf{path}$ es fácil de entender en este contexto, pero como no hay un ordenamiento único de las variables libres en $\mathsf{path}$ esto no es muy bonito, ¿o sí?

¿Alguna idea?

Answer 1

Bien, he encontrado una noción así con $[]$ -corchetes:

Escribimos

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

donde sustituimos $x \leftarrow v$ y $y \leftarrow w$ (por tanto, en el orden de los parámetros).

Además, escribimos por ejemplo

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

La noción se basa en la ordenación de los parámetros y en los distintos símbolos de la fórmula ( $x,y...$ ) y los símbolos del gráfico ( $v,w...$ ).