Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Without Loss of Generality: A limited of method of proof
40 views
Skip to first unread message
Message has been deleted
Dan Christensen
Nov 28, 2022, 2:23:33 PM11/28/22
to
INTRODUCTION
This 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. We can begin our proof by assumeing WITHOUT LOSS OF GENERALITY (WLOG) that x <= y. This means that we need to consider ONLY this case. If property P is symmetric, the following theorem tells us that we do NOT to consider the other case, namely that y <= x. It can save you several lines of proof.
WLOG can apparently be formally applied in many of situations. Here we discuss one of them.
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
Required property of <= on the reals:
1 ALL(a):ALL(b):[a in r & b in r => a<=b | b<=a]
Axiom
Suppose:
2 ALL(a):ALL(b):[a in r & b in r => [P(a,b) <=> P(b,a)]]
& ALL(a):ALL(b):[a in r & b in r => [a<=b => P(a,b)]]
Premise
Symmetry of P:
3 ALL(a):ALL(b):[a in r & b in r => [P(a,b) <=> P(b,a)]]
Split, 2
P holds for (a,b)
4 ALL(a):ALL(b):[a in r & b in r => [a<=b => P(a,b)]]
Split, 2
Suppose:
5 x in r & y in r
Premise
6 x in r
Split, 5
7 y in r
Split, 5
8 ALL(b):[x in r & b in r => x<=b | b<=x]
U Spec, 1
9 x in r & y in r => x<=y | y<=x
U Spec, 8
Two cases to consider:
10 x<=y | y<=x
Detach, 9, 5
Case 1
Suppose:
11 x<=y
Premise
12 ALL(b):[x in r & b in r => [x<=b => P(x,b)]]
U Spec, 4
13 x in r & y in 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)
Conclusion, 11
Case 2
Suppose:
17 y<=x
Premise
18 ALL(b):[y in r & b in r => [y<=b => P(y,b)]]
U Spec, 4
19 y in r & x in r => [y<=x => P(y,x)]
U Spec, 18
20 y in r & x in r
Join, 7, 6
21 y<=x => P(y,x)
Detach, 19, 20
22 P(y,x)
Detach, 21, 17
23 ALL(b):[y in r & b in r => [P(y,b) <=> P(b,y)]]
U Spec, 3
24 y in r & x in 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)
Conclusion, 17
30 [x<=y => P(x,y)] & [y<=x => P(x,y)]
Join, 16, 29
31 P(x,y)
Cases, 10, 30
As Required:
32 ALL(a):ALL(b):[a in r & b in r => P(a,b)]
Conclusion, 5
As Required:
33 ALL(a):ALL(b):[a in r & b in r => [P(a,b) <=> P(b,a)]]
& ALL(a):ALL(b):[a in r & b in r => [a<=b => P(a,b)]]
=> ALL(a):ALL(b):[a in r & b in r => P(a,b)]
Conclusion, 2
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
This 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. We can begin our proof by assumeing WITHOUT LOSS OF GENERALITY (WLOG) that x <= y. This means that we need to consider ONLY this case. If property P is symmetric, the following theorem tells us that we do NOT to consider the other case, namely that y <= x. It can save you several lines of proof.
WLOG can apparently be formally applied in many of situations. Here we discuss one of them.
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
Required property of <= on the reals:
1 ALL(a):ALL(b):[a in r & b in r => a<=b | b<=a]
Axiom
Suppose:
2 ALL(a):ALL(b):[a in r & b in r => [P(a,b) <=> P(b,a)]]
& ALL(a):ALL(b):[a in r & b in r => [a<=b => P(a,b)]]
Premise
Symmetry of P:
3 ALL(a):ALL(b):[a in r & b in r => [P(a,b) <=> P(b,a)]]
Split, 2
P holds for (a,b)
4 ALL(a):ALL(b):[a in r & b in r => [a<=b => P(a,b)]]
Split, 2
Suppose:
5 x in r & y in r
Premise
6 x in r
Split, 5
7 y in r
Split, 5
8 ALL(b):[x in r & b in r => x<=b | b<=x]
U Spec, 1
9 x in r & y in r => x<=y | y<=x
U Spec, 8
Two cases to consider:
10 x<=y | y<=x
Detach, 9, 5
Case 1
Suppose:
11 x<=y
Premise
12 ALL(b):[x in r & b in r => [x<=b => P(x,b)]]
U Spec, 4
13 x in r & y in 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)
Conclusion, 11
Case 2
Suppose:
17 y<=x
Premise
18 ALL(b):[y in r & b in r => [y<=b => P(y,b)]]
U Spec, 4
19 y in r & x in r => [y<=x => P(y,x)]
U Spec, 18
20 y in r & x in r
Join, 7, 6
21 y<=x => P(y,x)
Detach, 19, 20
22 P(y,x)
Detach, 21, 17
23 ALL(b):[y in r & b in r => [P(y,b) <=> P(b,y)]]
U Spec, 3
24 y in r & x in 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)
Conclusion, 17
30 [x<=y => P(x,y)] & [y<=x => P(x,y)]
Join, 16, 29
31 P(x,y)
Cases, 10, 30
As Required:
32 ALL(a):ALL(b):[a in r & b in r => P(a,b)]
Conclusion, 5
As Required:
33 ALL(a):ALL(b):[a in r & b in r => [P(a,b) <=> P(b,a)]]
& ALL(a):ALL(b):[a in r & b in r => [a<=b => P(a,b)]]
=> ALL(a):ALL(b):[a in r & b in r => P(a,b)]
Conclusion, 2
Dan
Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com
Mostowski Collapse
Nov 28, 2022, 5:03:17 PM11/28/22
to
Kind of climb down? So WLOG can be proved
nevertheless? Next step try proving this:
Lagrange's theorem (group theory)
left coset aH has the same cardinality as H
https://en.wikipedia.org/wiki/Lagrange's_theorem_%28group_theory%29
So you need only prove the cardinality of H once
and every left coset has the same cardinality.
Quite amazing, isn´t it?
nevertheless? Next step try proving this:
Lagrange's theorem (group theory)
left coset aH has the same cardinality as H
https://en.wikipedia.org/wiki/Lagrange's_theorem_%28group_theory%29
So you need only prove the cardinality of H once
and every left coset has the same cardinality.
Quite amazing, isn´t it?
Dan Christensen
Nov 28, 2022, 5:42:44 PM11/28/22
to
On Monday, November 28, 2022 at 5:03:17 PM UTC-5, Mostowski Collapse wrote:
> Kind of climb down? So WLOG can be proved
> nevertheless?
In a very limited way. Just a few special cases, each requiring a formal proof that would seem to consider every possible case. I'm still waiting for such a theorem to cover the colored beads problem in the Wikipedia article. We still have no formal proof that a WLOG proof will work in that case, not in any interesting way.
> Kind of climb down? So WLOG can be proved
> nevertheless?
> Next step try proving this:
>
> Lagrange's theorem (group theory)
> left coset aH has the same cardinality as H
Dan Christensen
Nov 29, 2022, 8:37:44 AM11/29/22
to
On Monday, November 28, 2022 at 2:23:33 PM UTC-5, Dan Christensen wrote:
> INTRODUCTION
>
> This 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. We can begin our proof by assumeing WITHOUT LOSS OF GENERALITY (WLOG) that x <= y. This means that we need to consider ONLY this case. If property P is symmetric, the following theorem tells us that we do NOT to consider the other case, namely that y <= x. It can save you several lines of proof.
>
> WLOG can apparently be formally applied in many of situations. Here we discuss one of them.
>
> 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
>
HTML version: https://www.dcproof.com/WithoutLossOfGenerality.htm
> INTRODUCTION
>
> This 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. We can begin our proof by assumeing WITHOUT LOSS OF GENERALITY (WLOG) that x <= y. This means that we need to consider ONLY this case. If property P is symmetric, the following theorem tells us that we do NOT to consider the other case, namely that y <= x. It can save you several lines of proof.
>
> WLOG can apparently be formally applied in many of situations. Here we discuss one of them.
>
> 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
>
Daven Ferrero
Nov 29, 2022, 12:17:02 PM11/29/22
to
Dan Christensen wrote:
> On Monday, November 28, 2022 at 2:23:33 PM UTC-5, Dan Christensen wrote:
>> INTRODUCTION => ALL(a):ALL(b):[a in r & b in r => P(a,b)] <--- P(a,b)
> On Monday, November 28, 2022 at 2:23:33 PM UTC-5, Dan Christensen wrote:
>> holds for all real numbers and b
>
> HTML version: https://www.dcproof.com/WithoutLossOfGenerality.htm
you stupid capitalist, they rise up and will burn you up like the witches,
>
> HTML version: https://www.dcproof.com/WithoutLossOfGenerality.htm
public places, for the severe crimes against humanity you commit. You
dirty philanthrope capitalist. You cannot escape, bitch. There is no
*amnesty* for nazi trash like you.
Which Spirit Do They Speak With
https://%62%69%74%63%68%75%74%65.com/%76%69%64%65%6f/AADt4MxkSbYa
Nick Arnolfi
Nov 29, 2022, 12:21:59 PM11/29/22
to
Dan Christensen wrote:
>> => ALL(a):ALL(b):[a in r & b in r => P(a,b)] <--- P(a,b) holds for all
>> real numbers and b
>>
> HTML version: https://www.dcproof.com/WithoutLossOfGenerality.htm
what people does with capitalists.
>> => ALL(a):ALL(b):[a in r & b in r => P(a,b)] <--- P(a,b) holds for all
>> real numbers and b
>>
> HTML version: https://www.dcproof.com/WithoutLossOfGenerality.htm
https://google.com/%73%65%61%72%63%68?q=%6d%65%64%69%65%76%61%6c%2b%62%75%72%6e%69%6e%67%2b%77%69%74%63%68%65%73&source=lnms&tbm=isch
Dan Christensen
Nov 29, 2022, 12:45:28 PM11/29/22
to
On Tuesday, November 29, 2022 at 12:17:02 PM UTC-5, Daven Ferrero wrote:
> Dan Christensen wrote:
>
> > On Monday, November 28, 2022 at 2:23:33 PM UTC-5, Dan Christensen wrote:
> >> INTRODUCTION => ALL(a):ALL(b):[a in r & b in r => P(a,b)] <--- P(a,b)
> >> holds for all real numbers and b
> >
> > HTML version: https://www.dcproof.com/WithoutLossOfGenerality.htm
> you stupid capitalist, they rise up and will burn you up like the witches,
You mean like they are going to do to your favourite capitalist, the Nazi Putin? You and your boss will be hunted as war criminals, Nazi Boy. Be ready.
> Dan Christensen wrote:
>
> > On Monday, November 28, 2022 at 2:23:33 PM UTC-5, Dan Christensen wrote:
> >> INTRODUCTION => ALL(a):ALL(b):[a in r & b in r => P(a,b)] <--- P(a,b)
> >> holds for all real numbers and b
> >
> > HTML version: https://www.dcproof.com/WithoutLossOfGenerality.htm
> you stupid capitalist, they rise up and will burn you up like the witches,
Mostowski Collapse
Nov 29, 2022, 1:30:16 PM11/29/22
to
There are now two WLOG proofs, your post here, and mine here:
> > > 76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
> > > Rem DNeg, 75
> > https://groups.google.com/g/sci.math/c/-p0Yr9Ja5io/m/dt4nFvW6BwAJ
Where is the limit? I don't see any limit. You didn't describe
when the limit is hit. What prevents one from understanding
in context what a mathematician says except your blockhead?
> > > 76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
> > > Rem DNeg, 75
> > https://groups.google.com/g/sci.math/c/-p0Yr9Ja5io/m/dt4nFvW6BwAJ
Where is the limit? I don't see any limit. You didn't describe
when the limit is hit. What prevents one from understanding
in context what a mathematician says except your blockhead?
Message has been deleted
Dan Christensen
Nov 29, 2022, 2:22:31 PM11/29/22
to
On Tuesday, November 29, 2022 at 1:30:16 PM UTC-5, Mostowski Collapse wrote:
> Dan Christensen schrieb am Montag, 28. November 2022 um 23:42:44 UTC+1:
> > On Monday, November 28, 2022 at 5:03:17 PM UTC-5, Mostowski Collapse wrote:
> > > Kind of climb down? So WLOG can be proved
> > > nevertheless?
> > In a very limited way. Just a few special cases, each requiring a formal proof that would seem to consider every possible case. I'm still waiting for such a theorem to cover the colored beads problem in the Wikipedia article. We still have no formal proof that a WLOG proof will work in that case, not in any interesting way.
> > > Next step try proving this:
> > >
> > > Lagrange's theorem (group theory)
> > > left coset aH has the same cardinality as H
> > Go for it!
> Dan Christensen schrieb am Montag, 28. November 2022 um 23:42:44 UTC+1:
> > On Monday, November 28, 2022 at 5:03:17 PM UTC-5, Mostowski Collapse wrote:
> > > Kind of climb down? So WLOG can be proved
> > > nevertheless?
> > In a very limited way. Just a few special cases, each requiring a formal proof that would seem to consider every possible case. I'm still waiting for such a theorem to cover the colored beads problem in the Wikipedia article. We still have no formal proof that a WLOG proof will work in that case, not in any interesting way.
> > > Next step try proving this:
> > >
> > > Lagrange's theorem (group theory)
> > > left coset aH has the same cardinality as H
> > Go for it!
> There are now two WLOG proofs, your post here, and mine here:
>
> > > > 76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
> > > > Rem DNeg, 75
> > > https://groups.google.com/g/sci.math/c/-p0Yr9Ja5io/m/dt4nFvW6BwAJ
>
I proved the general formula:
>
> > > > 76 EXIST(p):EXIST(q):[~p=q & color(p)=color(q)]
> > > > Rem DNeg, 75
> > > https://groups.google.com/g/sci.math/c/-p0Yr9Ja5io/m/dt4nFvW6BwAJ
>
ALL(a):ALL(b):[a in r & b in r => [P(a,b) <=> P(b,a)]]
& ALL(a):ALL(b):[a in r & b in r => [a<=b => P(a,b)]]
=> ALL(a):ALL(b):[a in r & b in r => P(a,b)]
Where do you have any such of general formula, Jan Burse? I'm thinking that the problem is not really amenable to a WLOG proof after all.
> Where is the limit?
We really have only one special case (mine) here. A few others are presented in Harrison's paper (link above). Hardly a general theory of WLOG proofs.
Mostowski Collapse
Nov 30, 2022, 4:34:54 PM11/30/22
to
You could equally well claim Q.E.D. isn't formalizable.
Latin phrase quod erat demonstrandum,
https://en.wikipedia.org/wiki/Q.E.D.
Because like WLOG, it involves too much informal reasoning.
Here is an example, which you might also have a hard time
to replicate in DC Proof. Is it therefore not formalizable?
Here is an example:
COROLLARY 1.30
PROOF. Obvious from (1.27) and (1.29). ✷
https://www.jmilne.org/math/CourseNotes/AG.pdf
✷ = Q.E.D.
Latin phrase quod erat demonstrandum,
https://en.wikipedia.org/wiki/Q.E.D.
Because like WLOG, it involves too much informal reasoning.
Here is an example, which you might also have a hard time
to replicate in DC Proof. Is it therefore not formalizable?
Here is an example:
COROLLARY 1.30
PROOF. Obvious from (1.27) and (1.29). ✷
https://www.jmilne.org/math/CourseNotes/AG.pdf
✷ = Q.E.D.
Mostowski Collapse
Nov 30, 2022, 4:48:28 PM11/30/22
to
But reading John Harrison is surely a good idea. Only DC
Proof can hardly be compared to what John Harrison uses.
Because he is usally working with:
- He isn't shy to use higher order logic from time to time
- He isn't shy to use tactics from time to time
So unless you want to add these features to DC Proof, you
will possibly not be able to replicate most of his examples.
For example his theorem here:
(* ------------------------------------------------------------------------- *)
(* A generic "without loss of generality" lemma for symmetry. *)
(* ------------------------------------------------------------------------- *)
let WLOG_RELATION = prove
(`!R P. (!x y. P x y ==> P y x) /\
(!x y. R x y \/ R y x) /\
(!x y. R x y ==> P x y)
==> !x y. P x y`,
REPEAT GEN_TAC THEN DISCH_THEN
(CONJUNCTS_THEN2 ASSUME_TAC (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
STRIP_TAC THEN ASM_SIMP_TAC[]);;
https://github.com/jrh13/hol-light/blob/master/theorems.ml
Quantifies over R and P, that is it quantifies over predicate
symbols, how would you do that in DC Proof?
Mostowski Collapse
Nov 30, 2022, 4:58:31 PM11/30/22
to
The tactics of Wolfgang Schwartz tree tool prove
it in a blink. Only Wolfgang Schwartz tree tool cannot
quantify predicates either, so its only this theorem:
(∀x∀y(Pxy → Pyx) ∧ (∀x∀y(Rxy ∨ Ryx) ∧ ∀x∀y(Rxy → Pxy))) → ∀x∀yPxy is valid.
https://www.umsu.de/trees/#~6x~6y(Pxy~5Pyx)~1(~6x~6y(Rxy~2Ryx))~1(~6x~6y(Rxy~5Pxy))~5~6x~6yPxy
If you can quantifier predicates you can use a theorem
as a template for other theorems. It becomes more
generic. It can be instantiated by other predicates or
formulae. Thats why I intially asked "Why Sets?". Because
John Harrison, especially from his HOL Light background,
is more used in using higher order stuff, and predicates
is one of the rather easy higher order stuff. They usually
have only the type i -> o or in the present example you
can view them having the type i x i -> o, or even polymorphic
most likely, type A x A -> o, where A is some type.
it in a blink. Only Wolfgang Schwartz tree tool cannot
quantify predicates either, so its only this theorem:
(∀x∀y(Pxy → Pyx) ∧ (∀x∀y(Rxy ∨ Ryx) ∧ ∀x∀y(Rxy → Pxy))) → ∀x∀yPxy is valid.
https://www.umsu.de/trees/#~6x~6y(Pxy~5Pyx)~1(~6x~6y(Rxy~2Ryx))~1(~6x~6y(Rxy~5Pxy))~5~6x~6yPxy
If you can quantifier predicates you can use a theorem
as a template for other theorems. It becomes more
generic. It can be instantiated by other predicates or
formulae. Thats why I intially asked "Why Sets?". Because
John Harrison, especially from his HOL Light background,
is more used in using higher order stuff, and predicates
is one of the rather easy higher order stuff. They usually
have only the type i -> o or in the present example you
can view them having the type i x i -> o, or even polymorphic
most likely, type A x A -> o, where A is some type.
0 new messages