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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.