$\newcommand{\A}{\mathcal A}\newcommand{\L}{\mathcal L}\renewcommand{\phi}{\varphi}$In J. Donald Monk's "Mathematical Logic", the following definition regarding model satisfaction is given: (pp. 196)
Definition 11.5 For any formula $\phi$ in $\L$ and any $\L$-structure $\A$, we define $\phi^\A\subseteq \sideset{^\omega}{}A$: for any $x\in\sideset{^\omega}{}A\;(=\{\langle x_i\rangle_{i\in\omega}\mid x_i\in A\})$:
- $x\in(\sigma=\tau)^\A$ iff $\sigma^\A x=\tau^\A x$; (actually, it says $\tau^\A y$, but that seems to be a typo)
- $(\neg\phi)^A = \sideset{^\omega}{}A\setminus\phi^\A$
- $\vdots$
- $x\in(\forall v_i\phi)^\A$ iff for all $a\in A$, $x_a^i\in\phi^A$
If $x\in\phi^\A$, we say $\A\models\phi[x]$.
It is the notation ($x_a^i$) in the last bullet that isn't totally clear to me. From the standard definition of model satisfaction, I would expect something like $$x_a^i = \langle x_0,x_1,\ldots,x_{i-1},a,x_{i+1},\ldots\rangle$$ However, nowhere in the book I can find the clarification of this notation.
Question. Is there someone familiar either with this notation in general, or with Monk's notation in this book in particular, who can give the precise definition of $x_a^i$?
You are right; it seems that there is not the definition of this symbol in Monk's book.
$x\in\sideset{^\omega}{}A$ is a function form $ω$ to $A$, i.e. a sequence $⟨x_i⟩_{i∈ω}$.
On page 7 we may find several ways of denoting the value of function $f$ at argument $a$; one of them is $f^a$. Thus, $x^i_a$ must mean that the function $x$ at argument $i$ has value $a$.
Basically, it is what Tarski (Monk was a student of Tarski) defined as $x(k/a)$; see Alfred Tarski & Robert Vaught, Arithmetical extensions of relational systems (1956), page 83, with the first definition of satisfiability.