In the first order logic, I would like to know what is the simplest way of defining the substitution of a term to a variable in a formula. As it is defined obviously by induction on terms then on formulas, the only difficulty is for quantifiers.
Is the following correct ? Can we come by something simpler ?
If $F=\exists xG$, if $x_{i_0},\dots,x_{i_{s-1}}$ are exactly the variables $x_i$ the variables among $x_0,\dots,x_r$ such that $x_i$ is free in $\exists xG$, then the substitution of $t_0$ to $x_0$, ..., $t_r$ to $x_r$ in $F$ is :
$(\exists xG)\dfrac{t_0...t_r}{x_0...x_r}=\exists u\left[G\dfrac{t_{i_0},\dots,t_{i_{s-1}},u}{x_{i_0},\dots,x_{i_{s-1}},x}\right]$, where $u$ is the first variable not in $F$, $t_{i_0}$, ..., $t_{s-1}$.
The definition for $\forall xG$ is identical.
I ask simpler because the definition of the substitution of $t_0$ to $x_0$,..., $t_r$ to $x_r$ is with this definition intertwined with the one of $x_{i_0}$ to $t_{i_0}$, ..., of $x_{i_{s-1}}$ to $t_{i_{s-1}}$ and of $u$ to $x$. It is then conceptually difficult to understand how we can construct such a fonction.