HomePage RecentChanges

jorend

Jason Orendorff (myfirstname dot mylastname at gmail).

http://jorendorff.blogspot.com/

Existence of pi

"I started to work on a little something and quickly discovered the reason for this. Metamath defines π as the smallest positive zero of the sine function, but as yet it has no proof that any such number exists!" (Excerpt of Jason Orendorff's blog)

Reading this, I began to think about what it does mean that something exists in set.mm. Here are the answers that come to my mind:

I have perhaps forgotten some meanings.

So what would happen if the smallest positive zero of the sine function didn't exist ?

– fl 13-Dec-2006

In ZF set theory, the "existence" of a class A simply means that A is a set, or equivalently A e. V. The class V does not exist. On the other hand, the existence of pi is easy to show: use ltso, cnvso, and supex. But that doesn't help us much. The problem is to show that pi is a real number. I haven't found an "easy" way to show this; perhaps a different definition of pi would be better. Any suggestions would be appreciated. Or better, actual proofs. :) BTW if the smallest positive zero of the sine function didn't exist, then it is not hard to see from df-sup that pi, as it is currently defined, would simply equal the empty set. And, as a matter of curiosity only, the empty set is not a complex number in set.mm, although that is dependent on set.mm's particular Dedekind-cut construction and shouldn't be depended on (e.g. Quine gives a real number construction where the empty set is the number 0). – norm 13 Dec 2006

If you want to prove that π, as defined in set.mm, is a real number, then probably the most direct way is as follows:

1. Prove that sin is a continuous function. I'm not sure how much more infrastructure is needed to do that - certainly continuity is one of the active areas of development there.

2. Prove error bounds on truncating the power series of the sin function, analogous to ege2le3.

3. Implement a four-function calculator for rational numbers, so you can automatically compute approximate values for sin(2) and sin(4), accurate enough to prove that sin(2) > 0 and sin(4) < 0.

If you want to prove that 2 < π < 4, then what I'd recommend is developing the sinc function, and showing that sinc(x)>0 for 0 < x < 2.

Of course, once we have more calculus in place, it should be possible to prove that the value of π is a standard power series approximation, or even a spigot function. Then it should be practical to compute many digits of precision. – raph

Pi fans will be happy to know that as of today, π has been shown to be real in Metamath's set.mm database, and also that 2 < π < 4, thanks to the impressive work of Paul Chapman. – norm 23 Jan 2008

Injective, surjective

Jason's blog (continued)

"The book I'm reading (by Benjamin Pierce) offers “injective functions are monic in Set; surjective functions are epic” as a mnemonic, you know, to help you remember monic and epic. This has to be the worst mnemonic of all time. I just don't see anything helpful about it. Sur- means “under”. Epi- mean “on top of”. I can never remember the difference between injective and surjective to begin with." Jason's blog"

Neither do I. And I should: "applications injectives" and "surjectives" are the official terms in France for 1-to-1 and onto mappings ( http://spiral.univ-lyon1.fr/mathsv/cours/analyse/Chap1/c1p3D.html ). They are (seemingly) Bourbaki's creation. However "sur" doesn't mean "under" it means "on top of". Perhaps what Pierce had in mind when he gave his "mnemonic". – fl 25-Jan-2008