Formalizing without loss of generality Suppose, while writing a proof, we derive:
$\forall x,y (x\leq y) \vee (y\leq x)$
One may say: "without loss of generality, let $x\leq y$" and continue the proof.
My goal is to understand how to express that WOLOG formally. Is the following correct:
We can generalize $(x\leq y)$ to a binary function $F$ and say we've proved:
$\forall F,x,y F(x,y) \vee F(y,x)$
Then, when proving, we have two cases we need to prove:
$\forall F,x,y F(x,y)$ (Case 1)
$\forall F,x,y F(y,x)$ (Case 2)
We can split the proof into two paths we need to consider, Case 1 and Case 2, and prove the same statement $Q$ from both cases to continue. ($(A \vee B) \wedge (A \implies Q) \wedge (B \implies Q)) \implies Q$)
I believe you can commute variables that are quantified as long as all the quantifiers are the same type (All $\forall$ or all $\exists$).
Therefore we can rewrite Case 2, commuting $x$ and $y$ in its quantifiers, as:
$\forall F,y,x F(y,x)$ (Case 2b)
However, now Case 2b is the same as Case 1 (by substituting $x=y$ and $y=x$ at the same time), therefore showing that we only need to prove Case 1.
Therefore the key to WOLOG is changing the order of the quantified variables so that multiple $\vee$ cases are identical. Is this correct?

In order to maintain generality, one needs to instantiate to a name/variable that doesn’t have any assumptions tied to it, i.e. an arbitrary one. Suppose I have the following formulas as assumptions:{Ha,∀x(Fx->Gx),∀xFx}. It’s clear that ∀xGx follows from this, but since the name “a” occurs in our assumptions, in order to maintain generality we would need to instantiate ∀xFx to some other name, e.g. “b”. Then, we derive Fb->Gb, which yields Gb. Since we chose an arbitrary name, we can conclude ∀xGx.
