In the lambda calculus (typed and untyped) "capture-avoiding substitution" is often defined. But this doesn't rule out non-capture avoiding substitutions unless we require that all substitutions are capture avoiding.
So non-capture avoiding substitutions are sometimes ok, unless we rule them out. Is that correct? I am thinking of an example like the following, in which we use beta-reduction on the variable $j$ with the argument $(\kappa\,m\,s')$, and this reduction results in the $s'$ becoming bound by the quantifier
$(\lambda j,i, s.\; \forall s' [\pi(i)(s)(s') \to f\, m\, (a\,(\kappa \, m\, s')\,s')\,j \,s' ])\;\;\\[0.3cm]=_{\beta}(\lambda i, s.\; \forall s' [\pi(i)(s)(s') \to f\, m\, (a\,(\kappa \, m\, s')\,s')\,(\kappa\,m\,s') \,s' ])$
No, incorrect. Non-capture avoiding substitutions are ruled out in the sense that there is nothing that would give rise to them. We have in the definition of substitution:
The first clause covers the case where either nothing in $N$ gets captured by $\lambda y$ or there are no occurrences to be substituted anyway; the second clause does the bound renaming. If there is any clash between the variables, the definition automatically leads to bound naming. And that covers all the possible cases. A substitution clause where we could do
does simply not exist. What you did in your example doesn't match any of the patterns above and is thus just not a substitution.
The definition of substitution, like the deifinitions of lambda-terms or beta-reduction, is generative, meaning that every substitution must be derivable from the rules, or it doesn't exist. It's not that capturing substitution is explicitly disallowed, it's just that there is no case that would lead to something like this, and what's not covered by the substitution rules is not a substitution.