# 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]$

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$.

Related questions