What is the difference between Leibniz's Law phrased as a schema and as a second-order axiom? I have occasionally come across Leibniz's Law (left to right, ie the indiscernibility of identicals) written with schematic letters in the consequent, and occasionally with a bound predicate-variable taking the place of the schematic letters.  What is the relevant difference between these formulations?  If there is ongoing debate, any leads on relevant literature would be most helpful.
 A: Suppose, to fix ideas, we are doing arithmetic, i.e. our first-order variables run over numbers, and suppose our language is countable.
The schematic version of Leibniz's Law, applied in this context, in effect tells us that if the numbers $m$ and $n$ are equal, then a first-order predicate $\varphi$ is true of $m$ if and only it is true of $n$.
The second-order version of Leibniz's Law tells us that if the numbers $m$ and $n$ are equal, then for any property at all $m$ has it if and only it is $n$ has it.
The second-order principle is stronger because it applies to all uncountably many properties of properties [or if you like to think extensionally, all uncountably many sets of numbers] not just to the countably many properties that can be expressed by predicates in our language. Moreover, the second-order version seems to be what we want to say when we claim that that identicals are indiscernible: i.e. if $m$ and $n$ are the same they share all properties.
Or at least the second-order version seems to be what we want, if we can indeed make sense of the idea of there being arbitrary properties of the numbers [arbitrary sets of numbers] which exist even when we have no way of specifying them. There are general issues about whether we can do this, according to various brands of constructivist or predicativist. Classical realists will say that there isn't a problem.
For an excellent treatment of issues surrounding the use of second-order logic (from a defender), and a discussion of the added richness we get from second-order formulations of various principles, see Stewart Shapiro's classic book Foundations without Foundationalism: The Case for Second-Order Logic.
A: I take it that by the schematic formulation you mean a meta-language statement such as the following:


*

*For any $r+1$-place relation symbol $R$ of the object language the sentence $\forall x_1 \ldots x_r \forall xy(x =y \rightarrow (Rx x_1 \ldots x_r \leftrightarrow Ry x_1 \ldots x_r))$ is true in every model (for the language).  


The most apparent difference is that the schematic formulation doesn't give you Leibniz's Law in your object language. For any relation symbol it only gives you the truth of the statement that identical objects don't differ in satisfying the symbol.  
The second-order version, on the other hand, does provide an object level representation of the law. As a consequence one can use it as the beginning of a definition of the identity predicate, something that is not possible using the schematic version. 
I haven't come across any discussion of the differences between these formulations. There is a recent paper by Andrew Bacon about paradoxes that result when naive truth theories are combined with the schematic version: 
http://www-bcf.usc.edu/~abacon/papers/Some%20problems%20for%20naive%20truth%20theory.pdf
I haven't read it entirely yet, but it may be of interest to you.   
