# define simultaneous substitution recursively

Can you help me with my approach to the following task:

Define simultaneous substitution $\phi[\psi_1,...,\psi_k/p_1,...,p_k]$ recursively.

Usually we have recursive definitions about formulas, but I think here I have to define it rekursively on k?

base case - $k=1$.

$\phi[\psi_1/p_1] = \phi[\psi_1/p_1]$

recursive case - $k > 1$.

Let $p^'_k$ be a variable not in $\psi_i$ for all $i \in \{1,...,k-1\}$ and not in $\phi$.

$\phi[\psi_1,...,\psi_k/p_1,...,p_k] = \left(\left(\phi[p^'_k/p_k]\right)[\psi_1,...,\psi_{k-1}]\right)[p_k/p^'_k]$

-
No ... since you want to have simultaneous substitution (and not one after the other as in recursion on $k$), I think you have to do it by recursion on $\phi$. –  martini May 14 '12 at 19:25
@martini: But how to do it by recursion on $\phi$? Aim is to define simultaneous substitution so I can't use a simultaneous substitution e. g. in the recursive case $\phi = \phi_1 \circ \phi_2$ as $\phi[\psi_1,...,\psi_k/p_1,...,p_k] = \phi_1[\psi_1,...,\psi_k/p_1,...,p_k] \circ \phi_2[\psi_1,...,\psi_k/p_1,...,p_k]$ since simultaneous recursion isn't defined at this moment! –  steltjen May 14 '12 at 20:26
When you use resursion on formulas, you start with basic formulas. So in you recursive step above, you haven't defined substitution for $\phi$, but for $\phi_1$ and $\phi_2$. –  martini May 15 '12 at 4:33

For substitution, it helps to think of $\varphi$ as a tree (connectives = internal nodes, variables = leaves).

The substitution is essentially replacing the leaves $p_i$ with trees for the $\psi_i$.

If you want to do the recursion on the number of variables, you have to do it in three steps to make sure the later substitution doesn't effect the former ones. You can do this by using new names for variables in $\psi_i$s (i.e. use $q_i$ in place of $p_i$) so no $p_j$ appears in any $\psi_i$. Then after you have done step by step substitution you can change the new names back to the old ones. The goal here is to avoid a variable $p_j$ in a $\psi_i$ being replaced by $\psi_j$.

-