Formalizing without loss of generality

Question

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?

Answer 1

You are correct. The "WLOG" method of proof can apparently be formally applied in many of situations. Your example, for which I provide formal proof here, is but one possibility. (See references)

As in your example, if you want to prove that, for all real numbers $x$ and $y$, $P(x,y)$ is true, you can begin your proof by assuming without loss of generality (WLOG) that $x \leq y$. We can apply this method of proof if property $P$ is symmetric, saving possibly many lines of proof.

The following theorem can be used to implement the above "shortcut" in formal proofs:

$\forall a,b\in R:[P(a,b)\iff P(b,a)~~~~$ (Property P is symmetric on the reals)

$\land \forall a,b\in R:[a\leq b\implies P(a,b)]~~~~$ ($P(a,b)$ holds for $a\leq b$)

$\implies \forall a,b\in R: P(a,b)$

Formal Proof (33 lines)

References:

https://en.wikipedia.org/wiki/Without_loss_of_generality https://www.cl.cam.ac.uk/~jrh13/papers/wlog.pdf (Thanks for the link, @blargoner )

Answer 2

Inspired by Dan Christensen's now-deleted answer, let us formalize the problem of proving that if three objects are each painted either red or blue, then there must be at least two objects of the same color.

We begin with our premises. First, there are three objects: $\varphi_1 = \exists_{=3} := \exists_3 \wedge \neg\exists_4$, where $$ \exists_n := \exists v_0 \cdots \exists v_{n-1} \bigwedge_{i < j < n} v_i \ne v_j $$ formalizes the sentence, "There are at least $n$ objects." Next, we introduce two unary relation symbols, $r$ and $b$, to represent the property of being red or blue, respectively. We then have the premise $$ \varphi_2 = \forall x \, ((rx \vee bx) \wedge \neg(rx \wedge bx)), $$ stating that every object is either blue or red, but not both. For convenience, let us introduce an explicitly defined binary relation symbol, $s$, to representing the notion that two objects have the same color: $$ \varphi_3 = sxy \leftrightarrow (rx \wedge ry) \vee (bx \wedge by). $$ Let $X=\{\varphi_1,\varphi_2,\varphi_3\}$. We wish to construct a proof demonstrating that $X\vdash\psi$, where $$ \psi = \exists x \exists y \, ((x \ne y) \wedge sxy). $$ Not counting our explicitly defined $s$, which can be eliminated by reduction, our logical signature is simply $L=\{r,b\}$. Let us add a single constant symbol, $c$, to denote the so-called "first object", and consider the sentence, $rc$. Suppose we can find a proof demonstrating that $X,rc\vdash\psi$. The map from the set of formulas, $\mathcal{L}\{r,b,c\}$, to itself which replaces every instance of $r$ with $b$ and vice versa will map $X$ and $\psi$ to themselves (modulo logical equivalence), will map $rc$ to $bc$, and will map our proof to a proof that $X,bc\vdash\psi$. Since $bc\equiv_X\neg rc$ (meaning $bc$ and $\neg rc$ are logically equivalent given $X$), this provides a proof that $X,\neg rc\vdash\psi$. Together with our original proof, this gives $X\vdash\psi$. Hence, "without loss of generality," we simply need to prove that $X,rc\vdash\psi$.

Answer 3

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.