substituting variables in well-formed formulas. Consider the well-formed formual below, What do you get by substituting t for x? $\forall x (p(x,y) \land \forall y(p(y,x) \rightarrow \exists x (p(x,z) \land q(z)))$ are there any restrictions or is it just a straight substitute yielding $\forall t (p(t,y) \land \forall y(p(y,t) \rightarrow \exists t (p(t,z) \land q(z)))$

Def of _substitution_ :

> For atomic $α$, $α(t/x)$ is the expression obtained from $α$ by replacing the variable $x$ by $t$.
>
> $(¬α)(t/x)$ is $¬α(t/x)$
>
> ...
>
> $(∀y \ α) (t/x)$ is $∀y \ α$, if $x=y$, and $∀y \ α(t/x)$, if $x \
e y$ (and the same for $\exists$).

Thus, in order to know:

> What do you get by substituting $t$ for $x$ into : $∀x(p(x,y)∧∀y(p(y,x)→∃x(p(x,z)∧q(z))))$

we have to apply the above definition (the clause for $\forall$) and we have that:

> > $(∀x(p(x,y)∧∀y(p(y,x)→∃x(p(x,z)∧q(z)))))(t/x)$
>
> is:
>
>> $∀x(p(x,y)∧∀y(p(y,x)→∃x(p(x,z)∧q(z))))$.