INTRODUCTION
************
The "WLOG" method of
proof (explained here) can apparently be formally applied in many of situations.
Here we discuss but one of them.
The following theorem can be
used as a shortcut in proofs about pairs of real numbers. Suppose you want to
prove that, for all real numbers x and y, property P(x,y) is true. You can begin your formal proof by
assuming WITHOUT LOSS OF GENERALITY (WLOG) that x <= y. We can apply this
method of proof if property P is symmetric (i.e. P(a,b) => P(b,a)) saving
possibly many lines of proof.
References:
https://en.wikipedia.org/wiki/Without_loss_of_generality
https://www.cl.cam.ac.uk/~jrh13/papers/wlog.pdf
THEOREM
*******
ALL(a):ALL(b):[a
in r & b in r => [P(a,b) <=> P(b,a)]] <--- Property P is symmetric on the real numbers
& ALL(a):ALL(b):[a
in r & b in r => [a<=b => P(a,b)]]
<--- P(a,b) holds for a<=b
=> ALL(a):ALL(b):[a
in r & b in r => P(a,b)] <--- P(a,b) holds for all real numbers and b
By Dan Christensen
2022-11-29
FORMAL PROOF
************
Required property of <= on
the reals
Two cases: a<=b OR b<=a
1 ALL(a):ALL(b):[a e r & b e r => a<=b | b<=a]
Axiom
Prove: ALL(a):ALL(b):[a e r & b e r => [P(a,b) <=> P(b,a)]]
& ALL(a):ALL(b):[a e r & b e r => [a<=b => P(a,b)]]
=> ALL(a):ALL(b):[a e r & b e r => P(a,b)]
Suppose...
2 ALL(a):ALL(b):[a e r & b e r => [P(a,b)
<=> P(b,a)]]
&
ALL(a):ALL(b):[a e r & b e r => [a<=b => P(a,b)]]
Premise
Symmetry of P
3 ALL(a):ALL(b):[a e r & b e r => [P(a,b)
<=> P(b,a)]]
Split, 2
Initial assumption "without loss of generality"
4 ALL(a):ALL(b):[a e r & b e r => [a<=b => P(a,b)]]
Split, 2
Prove: ALL(a):ALL(b):[a e r & b e r => P(a,b)]
Suppose...
5 x e r & y e r
Premise
6 x e r
Split, 5
7 y e r
Split, 5
Apply property of <= on reals
8 ALL(b):[x e r & b e r => x<=b | b<=x]
U Spec, 1
9 x e r & y e r => x<=y | y<=x
U Spec, 8
Two cases to consider:
10 x<=y | y<=x
Detach, 9, 5
Case 1
Prove: x<=y => P(x,y)
Suppose...
11 x<=y
Premise
Apply initial assumption WLOG
12 ALL(b):[x e r & b e r => [x<=b => P(x,b)]]
U Spec, 4
13 x e r & y e r => [x<=y => P(x,y)]
U Spec, 12
14 x<=y => P(x,y)
Detach, 13, 5
15 P(x,y)
Detach, 14, 11
Case 1
As Required:
16 x<=y => P(x,y)
4 Conclusion, 11
Case 2
Prove: y<=x => P(x,y)
Suppose...
17 y<=x
Premise
Apply initial assumption WLOG
18 ALL(b):[y e r & b e r => [y<=b => P(y,b)]]
U Spec, 4
19 y e r & x e r => [y<=x => P(y,x)]
U Spec, 18
20 y e r & x e r
Join, 7, 6
21 y<=x => P(y,x)
Detach, 19, 20
22 P(y,x)
Detach, 21, 17
Apply symmetry of P
23 ALL(b):[y e r & b e r => [P(y,b) <=> P(b,y)]]
U Spec, 3
24 y e r & x e r => [P(y,x) <=> P(x,y)]
U Spec, 23
25 P(y,x) <=> P(x,y)
Detach, 24, 20
26 [P(y,x) => P(x,y)] & [P(x,y) => P(y,x)]
Iff-And, 25
27 P(y,x) => P(x,y)
Split, 26
28 P(x,y)
Detach, 27, 22
Case 2
As Required:
29 y<=x => P(x,y)
4 Conclusion, 17
Joining results for Cases Rule
30 [x<=y => P(x,y)] & [y<=x => P(x,y)]
Join, 16, 29
Apply Cases Rule
31 P(x,y)
Cases, 10, 30
As Required:
32 ALL(a):ALL(b):[a e r & b e r => P(a,b)]
4 Conclusion, 5
As Required:
33 ALL(a):ALL(b):[a e r & b e r => [P(a,b)
<=> P(b,a)]]
&
ALL(a):ALL(b):[a e r & b e r => [a<=b => P(a,b)]]
=>
ALL(a):ALL(b):[a e r & b e r => P(a,b)]
4 Conclusion, 2