WLOG and "by symmetry" arguments and the foundations of mathematics John Harrison's paper Without Loss of Generality raises the interesting point that although "without loss of generality"/"by symmetry" arguments are a common proof technique, there is no corresponding formal mathematical law, so that automated theorem provers must be extended to handle such arguments. 
If ATPs cannot handle WLOG arguments in formal logic, can humans? Is it impossible to prove the WLOG argument in the general case in any of the conventional foundational logics of mathematics? If so, then does this indicate a deficit or shortfall or is the WLOG argument A) too trivial, or B) too metalogical?
I will clarify what I mean by a WLOG argument. In mathematical logic, if a pair of objects $A$ and $B$ are known to be indistinguishable up to naming, it is immediate that a proof of any property $P$ of $A$ automatically implies $P(B)$ and, conversely, $P(B) \to P(A)$. Such "Without loss of generality" or "by symmetry" arguments are used almost everywhere in mathematics and to say that the reasoning is obvious would be an enormous understatement. 
(To be precise, I want to emphasize that WLOG doesn't apply when some property of the objects is unknown and, when discovered, assigned to each of the objects arbitrarily. For example, although the roots of a polynomial are indistinguishable in the sense that the coefficients are invariant over permutation of the roots, it may be possible to discover the set of values and then make an arbitrary assignment of values to names. Indistinguishability is not the same as uncertainty.)
It could be argued that WLOG arguments are, like the cut rule, superfluous since they are only used to avoid needless repetition. However, since one may be referring to an uncountable or larger set of objects the WLOG argument may be necessary for the existence of a proof of finite length.
Perhaps what is needed is some kind of an axiom to patch this hole up?
 A: The paper does not claim that automated theorem provers cannot handle the case of such arguments, and indeed shows how to formalize them. The fact is that humans do not write proofs in the same way that ATPs do - very much is left for the reader to do. Indeed, this often rises to the level of little lemmas that could have their own proofs, and the author may only hint at how one might prove them.
This is exactly the case when we say "without loss of generality" - we are alluding to an omitted proof. The lemma would generally be of the form:

There is some group of symmetries preserving the properties at hand in the problem. There exists a symmetry such that _____ properties hold.

And this is more or less what the theorems that linked paper proves amount to. The proof should be obvious to the reader, but not to a machine.
So, on one hand, we cannot patch this hole, because there is no overarching proof of every such lemma we might want. But, on the other hand, there really is no hole to begin with - it's just another thing we need to translate for the machine.
