Let's denote A[x/y], where A is a formula and [x/y] has the definition of substituting x in the place of y.
The substitution rules for formulas involving quantifiers are then the following in predicate logic:
($\exists$x A)[y/x] = $\exists$x A
($\exists$x A)[y\k] = $\exists$x A[y\k], if x,k not present in the formula
($\exists$x A)[y\k] =$\exists$u (A[x\u])[y\k], otherwise, where u is not present in the formula and [x\u] only takes place for free variables.
Can anyone explain intuitively where these rules come from? I would like to better understand why they are defined as such. (Some of the rules may contain errors)
I'm not sure to understand your symbolism...
1) $(∃x A)[y/x] = ∃x A$. In a nutshell : we cannot substitute a variable that is bound, i.e. that is in the scope of the quantifier $∃$ (the same with $\forall$)
2) I think that you are considering : $(∃x A)[k/y] = ∃x A[k/y]$, i.e. we replace a variable $y$ with a term $k$ into the formula. If $x,k$ are not present in the formula, then the leading quantifier has no "role" whatever, and then we can ignore it.
3) Must be : $(∃x A)[k/y] = ∃u (A[u/x])[k/y]$. In this case $x$ is present in $A$ and thus - in order to avoid mistakes - we first replace $x$ with a new variable $x$; this is : $∃u A[u/x]$.
Note : $u$ must not be present in $A$ nor in the term $t$.