I have been under the impression that I could substitute just about anything for the variables in any proven theorem (via universal instantiation logic rule) but when applied to the Archimedean property:
If $x\in R$, $y\in R$, and $x>0$, then there is a positive integer $n$ such that $nx>y$
Substitute $y=nx$
you obtain $nx>nx$ which clearly does not hold.
What is the restriction to universal instantiation that prevents this?
On
To use universal instantiation, you substitute from the outside in. If you are looking to substitute for $y$, we must be starting with
$$(\forall y)(\forall x)[ x > 0 \to (\exists n) [ nx > y]]$$
You are asking about the restriction that prevents the term $nx$ from being substituted for $y$. The restriction on universal generalization, informally put, is that no variable in the term you are substituting can become bound when you perform the substitution. In this case both $n$ and $x$ become bound, so $nx$ is not substitutiable for $y$ here.
For a formal definition of "substitutable", see a logic text, or this question.
There is another way of formalizing universal instantiation, as in the Wikipedia article, so that there is no restriction on the term, but the substitution operation is changed so that if any variable in the new term was going to get bound, then that particular instance of the original variable is not substituted. However, for this variation to be useful, we would want to replace all instances of the original variable, which leads to the same restriction in practice.
It needs no restriction. The integer $n$ in $nx$ and the integer $n$ given by Archimedean property need not be same. Your statement would read