The sheet of equivalences given to us in class provides the two equivalences
\begin{array}{|c|c|c|} \hline \text{Universal Instantiation} & \forall x ~ P(x) \implies {S_t}^x P & \exists y ~ \forall x ~ P(x) \implies \exists y ~{S_t}^x P \\ \hline \text{Existential Instantiation} & \exists x ~ P \implies {S_t}^x P & \forall y ~ \exists x ~ P \implies {S_{A(y)}}^x P\\ \hline \end{array}
1. Does the structure $S_t^x P$ imply Skolemization of $x$ to some new constant $t$? Is this Skolemization sometimes written as $x/t$?
2. Is there a difference in meaning between $P(x)$ and $P$ between Universal and Existential Instantiation?
3. Does the notation $S_{A(y)}^x$ read as "replace the constant $x$ with some function $A(y)$", is this still considered Skolemization?
