Variable Assignment

A variable assignment is a function that assigns free variables (not constants) to a universe. Essentially, it assigns values to variables that are not already bound by a quantifier. Variable assignments are often coupled with an interpretation function to allow them to also assign terms.

Definition §

Variable Assignment

A variable assignment, $v$, is a function:

$$v:X_{free}\to D\subseteq \mathcal{U}$$

$$v(x_1,x_2,\dots ):\{x_1\mapsto u_1,x_2\mapsto u_2,\dots \}$$

• $X_{free}$ is the set of all free variables
  • $x$ is any free variable (not already bound by a quantifier)
• $D$ is a subset of the universe, $\mathcal{U}$ that $v$ maps onto
  • $u$ is some element in said universe (so can also be constants)

On-the-fly Variable Assignments ^definition-on-the-fly-assignment

If an extra mapping for a variable assignment, $v$ , needs to be added on the go (or is needed to create one if it is not already made) then a notation that can be used is:

$$v_{y\mapsto c}(x)=\{\begin{array}{ll}c,& x=y\\ v(y),& \text{else}\end{array}$$

It can be thought as a function wrapper, we ‘wrap’ an extra mapping on $v$, or as function composition. It can be likened to method overriding in programming.

Extending via Interpretation §

By themselves, variable assignments only map free variables. However, if combined with an interpretation, it can be extended to become applicable to terms as well.

A term is quite literally either a variable (which a normal variable assignment covers), a constant (which is covered by the interpretation) or a function (again, covered by interpretation). Hence, we can take a function, $f$, of several free variables $x,y,z\dots$ and interpret them using this interpretation.

$$v(c)\underset{\mathcal{I}}{\to }{c}^{\ast }\in \mathcal{U}$$

$$v(\underset{\text{Uninterpreted}}{\underbrace{f(x_1,x_2,\dots x_n)}})\underset{\mathcal{I}+v}{\to }{f}^{\ast }(v(x_1),v(x_2)\dots ,v(x_n))$$

• $c^{\ast }$: The constant $c$ after being interpreted by $\mathcal{I}$
• $f^{\ast }:{\mathcal{U}}^n\to \mathcal{U}$ is the function $f$ after being interpreted by $\mathcal{I}$
• $v(x\dots z)$ is the variables after being assigned.

Examples §

Example: Black & White §

Let the variable assignment be $v=\{x\mapsto \text{white}\}$.

Then $W(x)$ is true under $v$.

Also by extending via interpretation, we can also obtain formulae like $W(S(x))$, which works because we can ‘distribute’ the interpretation:

$$W(S(x))=W(S(\text{white}))=W(\text{black})=\perp$$