What is the real/'everyday-life' difference between free and bound variables My textbook is A Mathematical Introduction to Logic, 2nd Edition by Enderton.
The question initially comes when I was trying to prove Exercise 4. on pg.99
$$\text{Show that if }x \text{ does not occur free in }\alpha,\text{ then }\alpha \vDash \forall x \alpha$$
One of the lines in the proof, which as I worked out is:
the assignment functions $s$  and $s(x|d)$ agree on any variable but $x$, since $x$ does not occur free in $\alpha,$ hence
$$\vDash_\mathfrak{U} \alpha[s] \Leftrightarrow \vDash_{\mathfrak{U}}\alpha[s(x|d)]$$
Then, I referred back to Theorem 22A, which states:
Assume $s_1,s_2$ are assignment functions from $V$ into $\mathfrak{U}$ which agree at all variables (if any) that occur free in the wff $\phi$. Then
$$\vDash_{\mathfrak{U}} \phi[s_1] \Leftrightarrow \vDash_{\mathfrak{U}} \phi[s_2]$$
My question is that why only free variables are enough? Why don't we need to impose the agreement on the bound variables of $s_1,s_2$?
The proof of this theorem uses induction, where the inductive hypothesis simply states the agreement on free variables rather than telling the intuition behind it.
I attempted to answer my own question, but when it comes to discerning the difference between free and bound variables, the sentence 'a bound variable is a variable that's being quantified' feels incomplete, could you please provide richer insights to this?
Also,  this question is closely related to the post:
Show that if $x$ does not occur free in $α$, then $α \vDash ∀ x α$.
 A: In "everyday-life" there are no free variables.
In the language of predicate logic a free variable works like a pronoun in natural language: $\text{red}(x)$ is like "it is red". Its meaning depends on the context.
How we specify the "context" in predicate logic? With variable assignment functions:

$\mathfrak A,s \vDash \text {red}(x)$

holds if the chosen interpretation $\mathfrak A$ is my desk and the variable assignment function $s$ maps the variable $x$ occurring free to my red pencil.

The variable assignment function mechanism is a mathematical "trick" to define the semantical specifications of the language.
The recursive clauses for quantifiers reduce the satisfaction of the formula to the cases without quantifiers, i.e. to formulas with free variables.
The result that you refer to (Theorem 22A) simply amounts to proving that what matter in the semantical "valuation" of a formula are only the variables that occur free in it, and not all other infinite many variables of the language.
Maybe a simple example will help.
Consider the formula $(x=0)$ and the domain $\mathbb N$. If we consider a variable assignment function $s$ such that $s(x)=0$, we have that $\mathbb N,s \vDash (x=0)$; if instead we consider $s'$ with $s'(x)=1$ we will have that $\mathbb N,s' \nvDash (x=0)$.
Consider now the following two functions: $s$ such that $s(x)=0$ and $s(y)=1$ and $s'$ such that $s'(0)=1$ and $s'(y)=0$: do you see any change?
A: I don't really like to talk about bound variables, because it is rather about bound occurences of variables.
The main idea is that everything you derived are valid formulas.(Theorem of correctness)
Valid formulas are precisely those which are true under any interpretation of variables, functional and predicate symbols. (So terms and formulas have precise meaning(semantics)).
Different interpretations allow you to implement substitution operation, so you can obtain.
So essentially free [occurences of] variables are those which you can substitute without breaking the validity of a formula. Bound [occurences of] variables are all the rest.
