In Enderton pgs 83-84, he provides a recursive definition for satisfaction in FOL. I am having trouble understanding the clause regarding quantified sentences in FOL.
Let $s:\mathcal{V}\longmapsto|\mathfrak{A}|$, where $\mathcal{V}$ is the set of all variables and $|\mathfrak{A}|$ is the domain of the structure $\mathfrak{A}$.
The clause relating to quantified sentences runs as follows:
$\vDash_\mathfrak{A}\forall x\phi[s]$ iff for every $d\in|\mathfrak{A}|,\vDash_\mathfrak{A}\phi s(x|d) $
And this is how Enderton explains $s(x|d)$:
$s(x|d)$ is exactly like $s$ except for one thing: At the variable $x$, $s(x|d)$ assumes the value $d$.
Also, for clarity, earlier he says informally:
$\vDash_\mathfrak{A}\phi[s]$ iff the translation of $\phi$ determined by $\mathfrak{A}$, where the variable $x$ is translated as $s(x)$ wherever it occurs free, is true.
Intuitively, I understand perfectly what satisfaction requires when it comes to universally quantified sentences. Where I am struggling is on the role played here by $s(x|d)$ in the recursive definition. $s$ is a function that maps all of the variables onto members of the domain. So, the value of $s(x)$ is a member of the domain. And according to Enderton $s(x|d)$ does the same thing. That is, for all variables $y$, the value of $s(x|d)(y)$ is also a member of the domain. Indeed the same member $s(y)$ returns for that variable, unless the variable is $x$, then $s(x|d)(x)=d$.
Part of my confusion is that I don't really understand what $s(x|d)(x)=d$ means. Is $d$ one of the variables here, or is it one of members of the domain? And if the latter, which one? And lastly, I don't see how this move mechanically achieves the intuitive notion of satisfaction for quantified sentences in FOL.
Thanks for all the help. I really appreciate it!
Recall that $s : \text {Var} ⟼ |\mathfrak A|$, where $\text {Var}$ is the set of all variables and $|\mathfrak A|$ is the domain of the structure $\mathfrak A$.
Thjus, $s$ is a function that maps variables into objects of the domain.
What is $d$? An object of the domain: $d \in |\mathfrak A|$.
Thus, if we have a variable assignment function $s$, we will have that:
This is the gist of: "$s(x|d)$ is exactly like $s$ except for one thing: at the variable $x$ it assumes the value $d$."
Exactly because we want that $\forall x P(x)$ is true in a structure when the "meaning" of the predicate $P$ holds of every object in the domain of the structure.
Thus, whatever is the value of $s$ for variable $x$, we want that $s$ satisfies $P(x)$ in the structure.