From: Charlie-Boo on
On Jun 26, 3:01 am, William Hale <h...(a)tulane.edu> wrote:
> In article
> <2c95d415-5346-4aa9-855d-5ab834128...(a)i28g2000yqa.googlegroups.com>,
>
>  Charlie-Boo <shymath...(a)gmail.com> wrote:
> > On Jun 18, 9:12 pm, George Greene <gree...(a)email.unc.edu> wrote:
> [cut]
> > > Why is 1+1=2??
>
> > Lemme see . . .
>
> > Thm. 1+1=2
> > 1. 1=0'                Definition of syntax 1
> > 2. 2=1'                Definition of syntax 2
> > 3. 2=0''               Sub 1: 1 => 0' in 2
> > 4. (0')'=0''            Definition of syntax ()
> > 5. 0'+0=0'           Sub a+0=a (PA): a => 0'
> > 6. (0'+0)'=0''        Sub 5: 0' => 0'+0 in 4
> > 7. 0'+0' = (0'+0)'  Sub a+b' = (a+b)' (PA): a=>0' , b=>0
> > 8. (0'+0')=0''        Sub 7: (0'+0)' => 0'+0' in 6
> > 9. 1+1=2             Sub 1: 0' => 1, 3: 0'' => 2 in 8
> >    qed
>
> > Now who said that it takes 1,000 steps?  Those idiots Whitehead and
> > Russell (who said the way to resolve his Russell paradox was to outlaw
> > self-reference!) or the idiot with the MetaMath web site?  And they
> > never heard of Occam's Razor??
>
> A similar complaint could be made about Turing Machines. It would be a
> long program to code up an algorithm to add up two natural numbers.

No, the point is that it does NOT take 1,000 steps. If someone showed
you a TM that took 1,000 steps to perform addition, then he would be
wise to look at the TM that takes only 25.

But unfortunately, people forget about Occam's Razor and in fact act
the opposite: That a long complex proof is more impressive than the
smarter short one.

> Likewise, using Church's lambda calculus, it would be difficult to code
> up problems that are routinely given in a beginner's computer
> programming course.

You're talking two different systens. The 1,000 line proof and the 8
line proof are both (supposed) examples of axiomatic proofs in logic.
In fact, I used the same axioms, Peano's. We are not comparing
different systems. We are looking at a simple theorem with a simple
proof, and those who give a 1,000 line proof, or are impressed with
it, lack Mathematical sophistication.

> Yet, both of these are of importance. But, I suspect that you might say
> they are not.

Do you often draw inferences based on suspicions?

>
>
> > It takes 1,000 steps if you add unneeded lower level details.
>
> Rather, it takes 1,000 steps if you add needed lower level details. That
> is one of the points.

My proof is based on Peano's axioms and definitions of syntax. There
is no detail below axioms.

Do you see any advantage of an 8 line proof over a 1,000 line proof?
You are simply contradicting Occam. You are just a "fame worshiper".

> > But by
> > that reasoning, every proof in mathematics takes 1,000 steps.  All
> > could be expanded this way.
>
> > There is nothing special about 1+1=2 to make it take 1,000 steps.  Why
> > should it - it's simple as hell.  In fact, most math uses 1+1=2 so all
> > of them need 1,000 steps in their proofs as well.
>
> If you can give a simple proof from the ZFC axioms that 1 + 1 = 2,
> nobody would object. But, you gave a simple proof from the Peano axioms.

It is already a proof using ZFC since ZFC includes Peano's axioms.

> That is like somebody giving the Haskell program "add x y = x + y" when
> the question was to give a Turing machine program for the "add" function.

There is only one question: How to prove 1+1=2 from Peano's axioms.
The true scientist is a skeptic and doubts the effectiveness of a
1,000 line proof - especially after seeing an 8-line proof of the same
theorem.

C-B

> - Show quoted text -

From: William Hale on
In article
<37402b0d-57d8-479b-b6e6-11d27b6c4648(a)e5g2000yqn.googlegroups.com>,
Charlie-Boo <shymathguy(a)gmail.com> wrote:

> On Jun 26, 3:01�am, William Hale <h...(a)tulane.edu> wrote:
> > In article
> > <2c95d415-5346-4aa9-855d-5ab834128...(a)i28g2000yqa.googlegroups.com>,
> >
> > �Charlie-Boo <shymath...(a)gmail.com> wrote:
> > > On Jun 18, 9:12 pm, George Greene <gree...(a)email.unc.edu> wrote:
> > [cut]
> > > > Why is 1+1=2??
> >
> > > Lemme see . . .
> >
> > > Thm. 1+1=2
> > > 1. 1=0' � � � � � � � �Definition of syntax 1
> > > 2. 2=1' � � � � � � � �Definition of syntax 2
> > > 3. 2=0'' � � � � � � � Sub 1: 1 => 0' in 2
> > > 4. (0')'=0'' � � � � � �Definition of syntax ()
> > > 5. 0'+0=0' � � � � � Sub a+0=a (PA): a => 0'
> > > 6. (0'+0)'=0'' � � � �Sub 5: 0' => 0'+0 in 4
> > > 7. 0'+0' = (0'+0)' �Sub a+b' = (a+b)' (PA): a=>0' , b=>0
> > > 8. (0'+0')=0'' � � � �Sub 7: (0'+0)' => 0'+0' in 6
> > > 9. 1+1=2 � � � � � � Sub 1: 0' => 1, 3: 0'' => 2 in 8
> > > � �qed
> >
> > > Now who said that it takes 1,000 steps? �Those idiots Whitehead and
> > > Russell (who said the way to resolve his Russell paradox was to outlaw
> > > self-reference!) or the idiot with the MetaMath web site? �And they
> > > never heard of Occam's Razor??
> >
> > A similar complaint could be made about Turing Machines. It would be a
> > long program to code up an algorithm to add up two natural numbers.
>
> No, the point is that it does NOT take 1,000 steps. If someone showed
> you a TM that took 1,000 steps to perform addition, then he would be
> wise to look at the TM that takes only 25.

You misunderstood my comparison. I am not comparing Turing coding to
writing proof for "1+1=2". My comparison is: your Peano proof is to the
ZFC proof as mine Haskell coding of addition is to a Turing coding of
addition. The Haskell program coding is "add x y = x + y", while the
Turing coding would take hundreds of lines of instructions (I suspect).
Even if the TM coding took only 25 instructions, it still would be 25
times longer than the Haskell coding.

>
> But unfortunately, people forget about Occam's Razor and in fact act
> the opposite: That a long complex proof is more impressive than the
> smarter short one.

Nobody claims this.

> > Likewise, using Church's lambda calculus, it would be difficult to code
> > up problems that are routinely given in a beginner's computer
> > programming course.
>
> You're talking two different systens.

Of course I am talking about two different systems. I said a similar
complaint about "length" of proof in the two axiomatic systems could
likewise be made about "length" of coding in two programming systems.

> The 1,000 line proof and the 8
> line proof are both (supposed) examples of axiomatic proofs in logic.
> In fact, I used the same axioms, Peano's.

As has been mentioned over and over again, the axioms of Peano are not
the axioms of ZFC, and they are in no way related to one another. One is
not a subset of the other.

> We are not comparing different systems.

Yes we are. Peano has 5 or so axioms, while ZFC has 10 or more axioms.
This is just looking at a count of the axioms. If you read the axioms,
you can see that they are not even similar.

> We are looking at a simple theorem with a simple
> proof, and those who give a 1,000 line proof, or are impressed with
> it, lack Mathematical sophistication.
>
> > Yet, both of these are of importance. But, I suspect that you might say
> > they are not.
>
> Do you often draw inferences based on suspicions?

I was trying to anticipate your answer to speed up the discussion since
these discussions drag on so long. Unfortunately, you didn't state your
opinion on programming with TM as opposed to programming in Haskell. I
still don't know whether you object to people presenting a TM program to
do addition by exhibiting a 25 line TM program when one could give a one
line Haskell program to do the same thing.

That is, I was admitting that my argument would carry no weight for you
since I suspected that you would say the 25 line TM program is just as
stupid as the 1000 line ZFC proof because the program can be done in one
line in Haskell and the proof could be done in 10 lines in PA.

> >
> > > It takes 1,000 steps if you add unneeded lower level details.
> >
> > Rather, it takes 1,000 steps if you add needed lower level details. That
> > is one of the points.
>
> My proof is based on Peano's axioms and definitions of syntax. There
> is no detail below axioms.

But the 1000 lines of proof is based on the ZFC axioms, not the PA
axioms.

>
> Do you see any advantage of an 8 line proof over a 1,000 line proof?

No. But, I see the advantages of ZFC over PA for doing mathematics. The
use of "sets" in mathematics has increased tremendously since the
1850's, and ZFC provides an axiomatic foundation for mathematics sets,
while PA does not.

> You are simply contradicting Occam. You are just a "fame worshiper".
>
> > > But by
> > > that reasoning, every proof in mathematics takes 1,000 steps. �All
> > > could be expanded this way.
> >
> > > There is nothing special about 1+1=2 to make it take 1,000 steps. �Why
> > > should it - it's simple as hell. �In fact, most math uses 1+1=2 so all
> > > of them need 1,000 steps in their proofs as well.
> >
> > If you can give a simple proof from the ZFC axioms that 1 + 1 = 2,
> > nobody would object. But, you gave a simple proof from the Peano axioms.
>
> It is already a proof using ZFC since ZFC includes Peano's axioms.

As has been mentioned over and over again, ZFC does not include the
Peano's axioms.

> > That is like somebody giving the Haskell program "add x y = x + y" when
> > the question was to give a Turing machine program for the "add" function.
>
> There is only one question: How to prove 1+1=2 from Peano's axioms.

No, there are two questions: 1) how to prove "1+1 = 2" from Peano's
axioms and 2) how to prove "1+1 = 2" from the ZFC axioms. In college,
most mathematicians, if not all, have proven statements similar to
"1+1=2" using Peano's axioms; few in college have proven statements
similar to "1+1=2" using ZFC axioms, since ZFC is not usually taught in
college. Most mathematicians learn ZFC on their own.

> The true scientist is a skeptic and doubts the effectiveness of a
> 1,000 line proof - especially after seeing an 8-line proof of the same
> theorem.
>
> C-B
>
> > - Show quoted text -
From: Charlie-Boo on
On Jun 26, 3:08 pm, William Hale <h...(a)tulane.edu> wrote:
> In article
> <37402b0d-57d8-479b-b6e6-11d27b6c4...(a)e5g2000yqn.googlegroups.com>,
>
>
>
>
>
>  Charlie-Boo <shymath...(a)gmail.com> wrote:
> > On Jun 26, 3:01 am, William Hale <h...(a)tulane.edu> wrote:
> > > In article
> > > <2c95d415-5346-4aa9-855d-5ab834128...(a)i28g2000yqa.googlegroups.com>,
>
> > > Charlie-Boo <shymath...(a)gmail.com> wrote:
> > > > On Jun 18, 9:12 pm, George Greene <gree...(a)email.unc.edu> wrote:
> > > [cut]
> > > > > Why is 1+1=2??
>
> > > > Lemme see . . .
>
> > > > Thm. 1+1=2
> > > > 1. 1=0' Definition of syntax 1
> > > > 2. 2=1' Definition of syntax 2
> > > > 3. 2=0'' Sub 1: 1 => 0' in 2
> > > > 4. (0')'=0'' Definition of syntax ()
> > > > 5. 0'+0=0' Sub a+0=a (PA): a => 0'
> > > > 6. (0'+0)'=0'' Sub 5: 0' => 0'+0 in 4
> > > > 7. 0'+0' = (0'+0)' Sub a+b' = (a+b)' (PA): a=>0' , b=>0
> > > > 8. (0'+0')=0'' Sub 7: (0'+0)' => 0'+0' in 6
> > > > 9. 1+1=2 Sub 1: 0' => 1, 3: 0'' => 2 in 8
> > > > qed
>
> > > > Now who said that it takes 1,000 steps? Those idiots Whitehead and
> > > > Russell (who said the way to resolve his Russell paradox was to outlaw
> > > > self-reference!) or the idiot with the MetaMath web site? And they
> > > > never heard of Occam's Razor??
>
> > > A similar complaint could be made about Turing Machines. It would be a
> > > long program to code up an algorithm to add up two natural numbers.
>
> > No, the point is that it does NOT take 1,000 steps.  If someone showed
> > you a TM that took 1,000 steps to perform addition, then he would be
> > wise to look at the TM that takes only 25.
>
> You misunderstood my comparison. I am not comparing Turing coding to
> writing proof for "1+1=2". My comparison is: your Peano proof is to the
> ZFC proof

ZFC contains PA so my 9 line proof in PA is also a 9 line proof in
ZFC.

> as mine Haskell coding of addition is to a Turing coding of
> addition. The Haskell program coding is "add x y = x + y", while the
> Turing coding would take hundreds of lines of instructions (I suspect).
> Even if the TM coding took only 25 instructions, it still would be 25
> times longer than the Haskell coding.
>
>
>
> > But unfortunately, people forget about Occam's Razor and in fact act
> > the opposite: That a long complex proof is more impressive than the
> > smarter short one.
>
> Nobody claims this.

People often highlight the huge proof of 1+1=2 in Principia
Mathematica, as does the MetaMath web site, when Occam tells us that
is a very poor design, and short proofs such as my 9 line proof are to
be preferred. It's a fairly famout bit of trivia.

> > > Likewise, using Church's lambda calculus, it would be difficult to code
> > > up problems that are routinely given in a beginner's computer
> > > programming course.
>
> > You're talking two different systens.
>
> Of course I am talking about two different systems. I said a similar
> complaint about "length" of proof in the two axiomatic systems

It's only one proof. ZFC contains PA and the 9 line proof in PA is a
9 line proof in ZFC.

> could
> likewise be made about "length" of coding in two programming systems.
>
> > The 1,000 line proof and the 8
> > line proof are both (supposed) examples of axiomatic proofs in logic.
> > In fact, I used the same axioms, Peano's.
>
> As has been mentioned over and over again, the axioms of Peano are not
> the axioms of ZFC, and they are in no way related to one another. One is
> not a subset of the other.

Peano's Axioms are used in ZFC proofs.

> > We are not comparing different systems.
>
> Yes we are. Peano has 5 or so axioms, while ZFC has 10 or more axioms.
> This is just looking at a count of the axioms. If you read the axioms,
> you can see that they are not even similar.
>
> > We are looking at a simple theorem with a simple
> > proof, and those who give a 1,000 line proof, or are impressed with
> > it, lack Mathematical sophistication.
>
> > > Yet, both of these are of importance. But, I suspect that you might say
> > > they are not.
>
> > Do you often draw inferences based on suspicions?
>
> I was trying to anticipate your answer to speed up the discussion since
> these discussions drag on so long. Unfortunately, you didn't state your
> opinion on programming with TM as opposed to programming in Haskell. I
> still don't know whether you object to people presenting a TM program to
> do addition by exhibiting a 25 line TM program when one could give a one
> line Haskell program to do the same thing.
>
> That is, I was admitting that my argument would carry no weight for you
> since I suspected that you would say the 25 line TM program is just as
> stupid as the 1000 line ZFC proof because the program can be done in one
> line in Haskell and the proof could be done in 10 lines in PA.
>
>
>
> > > > It takes 1,000 steps if you add unneeded lower level details.
>
> > > Rather, it takes 1,000 steps if you add needed lower level details. That
> > > is one of the points.
>
> > My proof is based on Peano's axioms and definitions of syntax.  There
> > is no detail below axioms.
>
> But the 1000 lines of proof is based on the ZFC axioms, not the PA
> axioms.
>
>
>
> > Do you see any advantage of an 8 line proof over a 1,000 line proof?
>
> No. But, I see the advantages of ZFC over PA for doing mathematics. The
> use of "sets" in mathematics has increased tremendously since the
> 1850's, and ZFC provides an axiomatic foundation for mathematics sets,
> while PA does not.
>
> > You are simply contradicting Occam.  You are just a "fame worshiper".
>
> > > > But by
> > > > that reasoning, every proof in mathematics takes 1,000 steps. All
> > > > could be expanded this way.
>
> > > > There is nothing special about 1+1=2 to make it take 1,000 steps. Why
> > > > should it - it's simple as hell. In fact, most math uses 1+1=2 so all
> > > > of them need 1,000 steps in their proofs as well.
>
> > > If you can give a simple proof from the ZFC axioms that 1 + 1 = 2,
> > > nobody would object. But, you gave a simple proof from the Peano axioms.
>
> > It is already a proof using ZFC since ZFC includes Peano's axioms.
>
> As has been mentioned over and over again, ZFC does not include the
> Peano's axioms.
>
> > > That is like somebody giving the Haskell program "add x y = x + y" when
> > > the question was to give a Turing machine program for the "add" function.
>
> > There is only one question: How to prove 1+1=2 from Peano's axioms.
>
> No, there are two questions: 1) how to prove "1+1 = 2" from Peano's
> axioms and 2) how to prove "1+1 = 2" from the ZFC axioms. In college,
> most mathematicians, if not all, have proven statements similar to
> "1+1=2" using Peano's axioms; few in college have proven statements
> similar to "1+1=2" using ZFC axioms, since ZFC is not usually taught in
> college. Most mathematicians learn ZFC on their own.
>
>
>
> > The true scientist is a skeptic and doubts the effectiveness of a
> > 1,000 line proof - especially after seeing an 8-line proof of the same
> > theorem.
>
> > C-B
>
> > > - Show quoted text -- Hide quoted text -
>
> - Show quoted text -- Hide quoted text -
>
> - Show quoted text -

From: William Hale on
In article
<7e830cd6-b698-4f19-9152-d361cbc1b04e(a)a30g2000yqn.googlegroups.com>,
Charlie-Boo <shymathguy(a)gmail.com> wrote:

> On Jun 26, 3:08�pm, William Hale <h...(a)tulane.edu> wrote:
> > In article
> > <37402b0d-57d8-479b-b6e6-11d27b6c4...(a)e5g2000yqn.googlegroups.com>,
> > �Charlie-Boo <shymath...(a)gmail.com> wrote:
[cut]
> > > But unfortunately, people forget about Occam's Razor and in fact act
> > > the opposite: That a long complex proof is more impressive than the
> > > smarter short one.
> >
> > Nobody claims this.
>
> People often highlight the huge proof of 1+1=2 in Principia
> Mathematica, as does the MetaMath web site, when Occam tells us that
> is a very poor design, and short proofs such as my 9 line proof are to
> be preferred. It's a fairly famout bit of trivia.

People often highlight the huge proof of 1+1=2 in Principia Mathematica
because it is complete in all the necessary detail, not because it is
huge.

Nobody claims that a long complex proof is more impressive than the
smarter short one. If your 9 line proof were correct in the axiom system
used by the Principia Mathematica, then people would use it because they
prefer smart short proofs. Since they don't quote your 9 line proof as
the preferred proof, the conclusion is not that they think a long
complex proof is more impressive than the smarter short one, but rather
that mathematicians are not good at mathematics.
From: Charlie-Boo on
On Jun 26, 3:57 pm, William Hale <h...(a)tulane.edu> wrote:
> In article
> <7e830cd6-b698-4f19-9152-d361cbc1b...(a)a30g2000yqn.googlegroups.com>,
>
>
>
>
>
>
>
>  Charlie-Boo <shymath...(a)gmail.com> wrote:
> > On Jun 26, 3:08 pm, William Hale <h...(a)tulane.edu> wrote:
> > > In article
> > > <37402b0d-57d8-479b-b6e6-11d27b6c4...(a)e5g2000yqn.googlegroups.com>,
> > > Charlie-Boo <shymath...(a)gmail.com> wrote:
> [cut]
> > > > But unfortunately, people forget about Occam's Razor and in fact act
> > > > the opposite: That a long complex proof is more impressive than the
> > > > smarter short one.
>
> > > Nobody claims this.
>
> > People often highlight the huge proof of 1+1=2 in Principia
> > Mathematica, as does the MetaMath web site, when Occam tells us that
> > is a very poor design, and short proofs such as my 9 line proof are to
> > be preferred.  It's a fairly famout bit of trivia.
>
> People often highlight the huge proof of 1+1=2 in Principia Mathematica
> because it is complete in all the necessary detail, not because it is
> huge.

So the rest of the proofs aren't??

No, they say "It takes 1,000 lines!" The give the last line of the
proof and say, "And that's on page 123!" Look at any reference to
it. With all the proofs in Principia Mathematica, why is that one
singled out?

As far as PA vs. ZFC goes:

Do you know how N is represented in ZFC? By constructing a
representation of numbers, a set that meets Peano's Axioms, and then
defining N to be that set. So they include Peano's Axioms with a
"definition" that N satisifies them. See any text - e.g. Set Theory
for the Working Mathematician, Ciesielski pg. 26-29.

C-B

> Nobody claims that a long complex proof is more impressive than the
> smarter short one. If your 9 line proof were correct in the axiom system
> used by the Principia Mathematica, then people would use it because they
> prefer smart short proofs.

On the MetaMath web site, the proof of 1+1=2 would take just a few
lines, so he gives the proof of 2+2=4 that takes the 1,000 lines!

> Since they don't quote your 9 line proof as
> the preferred proof, the conclusion is not that they think a long
> complex proof is more impressive than the smarter short one, but rather
> that mathematicians are not good at mathematics.- Hide quoted text -
>
> - Show quoted text -