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?