Question regarding Karp-Lipton theorem In the proof in wikipedia, it goes like this:

Let $L \in \Pi_{2}$, so we can describe membership in $L$ as a formula:

$\forall_{y}\exists_{z} V(x,y,z)=1 \iff x \in L$

(where V is polynomial deterministic verifier etc...)
Now they look at the subformula : $s(y)=\exists_{z} V(x,y,z)$ and say that because it's an instance of $SAT$, and according to the hypothesis that $NP \subseteq P/poly$, its equivalent to $C(s(y))$, where $C$ is a valid circuit for solving $SAT$.

These are my questions:


What does $s(y)$ mean? Like what's the meaning of saying that something equals some predicate? It look like merely a technical part of the proof but I can't wrap my head around it.
What's the meaning of exchanging a logical predicate with circuit evaluation mean? Does it mean that we can decide if for every $y$ there exists $z$ such that $V(x,y,z)=1$ with a circuit?
The subformula $s(y) = \exists z V(x,y,z)$ is a Boolean function which depends on $x$ and $y$. In this context we can assume that $x$ is fixed, so we only show the dependence on $s(y)$. Here $\exists z V(x,y,z)$ is the definition of the function: the value of $s$ on an input $y$ equals the truth value of the formula $\exists z V(x,y,z)$ (recall we're assuming that $x$ is fixed).

Since $V$ runs in polynomial time, as in Cook's theorem we can encode $V(x,y,z)$ is a polynomial size formula in the variables $x,y,z$. Given the fixed input $x$ and an input $y$, we can substitute $x$ and $y$ in the formula for $V(x,y,z)$ to get a formula $\varphi_{x,y}$ depending only on $z$. We can also convert this formula to CNF. The new formula is satisfiable, i.e. $s(y)$ is true, iff $\varphi_{x,y} \in SAT$.

If we have a circuit $C$ solving SAT we can use it to check whether $\varphi_{x,y}$ is satisfiable. That's what Wikipedia means when it writes $C(s(y))$: write $s(y)$ as an instance $\varphi_{x,y}$ of SAT, and then run $C$ on the instance to get the truth value of $s(y)$. Since $C$ solves SAT, $C(s(y)) = s(y)$, that is, on input $\varphi_{x,y}$ the circuit $C$ will output the truth value of $s(y)$.