Finally Here!

20 07 2006

Woohoo! After nearly 2 weeks, despite the claim of a 2 day delivery estimate, the book i recently ordered has finally arrived. I was so worried but now I am so happy. Yayyy.

Quote:

Reviews
Synopsis
Advanced undergraduate or beginning graduate students need a unified foundation for their study of geometry, analysis, and algebra. For the first time in a text, this book uses categorical algebra to build such a foundation, starting from intuitive descriptions of mathematically and physically common phenomena and advancing to a precise specification of the nature of Categories of Sets. Set theory as the algebra of mappings is introduced and developed as a unifying basis for advanced mathematical subjects such as algebra, geometry, analysis, and combinatorics. The formal study evolves from general axioms which express universal properties of sums, products, mapping sets, and natural number recursion. The distinctive features of Cantorian abstract sets, as contrasted with the variable and cohesive sets of geometry and analysis, are made explicit and taken as special axioms. Functor categories are introduced in order to model the variable sets used in geometry, and to illustrate the failure of the axiom of choice. An appendix provides an explicit introduction to necessary concepts from logic, and an extensive glossary provides a window to the mathematical landscape.

Cant wait to read it. :D





Numbers + Programs as Proofs

18 07 2006

I wanna cover things many people take for granted from an angle they are not used to. For example, I used to think vectors are directed line segments. Then i thought of them as members of an abstract vector space. Neither of these are correct because they both are…I plan to cover this by going over equivalence classes in a geometry in very clear english that requires no background in math beyond knowing how to count and basic geometry.

I also plan to continue by constructing the integers, rationals and then the reals. Go over interesting numbers like the “Number of Infinite Knowledge” and Unaccessible numbers and how to construct a number that cannot be constructed. And finally the hyperreals, which if youll notice I am trying to write on..they are quite useful for calculus.

I also hope to be motivated enough to cover the surreal numbers (drop back from hyperreals and extend reals with surreals), p-adic numbers (drop back to rationals and complete the rationals in a new way) and a new method i just read about which constructs a system isomorphic (equivallent) to the reals but skips the rationals and proceeds directly from the integers in its construction.
Numbers, numbers , numbers!!

_                ----->  "Eudoxus" numbers equivalent to reals
                |
Naturals --> Integers --> Rationals --> Reals --> Complex
                               |          |
                               |          |====>Hyperreals  <- both contain infinitesimals and infinite numbers
                               |          |===> Surreals
                               |---> p-adic

Programs as Proofs

In other news Im learning Coq, where you construct maths much the same way you write programs. In essence you are programming math theorems. Not only that, your mathematical proofs are guranteed to be logically correct and perfect if they are verified sucessfully (compile properly). This is a major bonus for peer review since they just need to briefly look over your proof (code) to make sure you didnt cheat in definitions (stuff like that) as opposesed to the weeks to sometimes months it takes now. I like this because I have always been enamored of Intuitionsitic logics and constructivism (which applies in this case).

Thanks to this Ive been learning alot about type theory and constructive logics so Im understanding alot of what those people in the Software engineering forums are saying more and more! Further on, thanks to curry-howard isomorphism your programs are identical to proofs. That means that you can write programs as a proof and Coq will extract OCaml (or scheme or haskell) code. Now, not only will your algorithim be guranteed to be syntatically correct, it will also be logically correct. Not only that, the Coq environment is a proof assister and can actually help you out and auto prove simple sections. And because you are working at a very highlevel with incredibly rich mathematical types, the going is just unimaginably fast (im talking many magnitudes here). Imagine it..proving your complete scenegraph in less than an hour (or more dependending on your skills) vs. implementing it in C++. Ill be sure to go over my experience. My first pet project may be a simple matrix library extracted to Ocaml which should work in F# too. I plan to take adavantage of this isomorphism extensively with my main project, prolly improve my effieciency by at least a factor of 20 :D. Hopefully I make up the time im losing learning this.

The only thing about Coq is that there is very little documentation on it. The only book on it costs £40 and there is only 1 tutorial on it on the entire internet. So im mostly having to learn off the reference manual and developments in its standard library. Its tough and slow going.

Some n00b proofs from a tutorial im following. One proves a simple proposition and the other proves that a transitive and symmetric relation is reflective. :

Quote:


Section Tr.
Variable A B C: Prop.Lemma d_a : A -> B /\ C -> (A -> B) /\ (A -> C).
split.
elim H0.intros. exact H1. elim H0. intros. exact H2. Qed.

Require Import utf8.
Section rr.

Variable A B: Set.

Variable f: A -> B.
Variable D: Set. Variable R : D -> D -> Prop.

Section R_sym_trans.
Hypothesis R_sym : ∀x y:D, R x y → R y x.
Hypothesis R_trans : ∀x y z:D, R x y → R y z→ R x z.

Lemma refl: ∀x:D, (∃y, R x y) → R x x.
intros. elim H.intros. apply R_trans with x0. assumption. apply R_sym.
assumption.

Also check out this link which contains lots of interesting interviews with great people. Lots of stuff to learn from there People’s Archive





Numbers: Part 1

9 07 2006

In this post I go over why numbers do not exist. Since in a way, we may say that they are pulled out of thin air. People in the olden days liked to lock themselves into certain dogmatic ways of thinking, something which has cursed the future generations into having more trouble with math concepts than need have been. You can tell the close mindedness of the people of old by their insistance to have such names as postive, negative, natural, rational, irrational, real and imaginary for number types.

The task of this post is to show that the imaginary number i is no more or no less real than the number 4. It is often that you will see people say such things as how can you have the square root of a negative number? Some even go as far as to ask how can you have negative money? This is due to a misunderstanding of what a number is.

On the first, how can you have issue with the root of a negative number? This is simply due to centuries old dogma passed traditionally from teacher to student in grade school with the idea that the positive integers are real or exist somewhere and that only they can be numbers. We are taught properties of integers and are told that only those that follow these rules are numbers. How silly. The second on negative money may be considered to be that the positive integers associations are more concrete. 5 -> cats. 1000 -> money. Numbers are no more than an abstract invention or tool we may attach to appropriate situatations which help us reason on certain things we encounter in nature.

We say 5 boxes and attach the concept of 5 to boxes which enable us to envision the multiple boxes. At 45443454 we can no longer even envision the boxes and simply have another concept, a vague notion of many boxes: 454454 -> vague concept -> many concrete objects: boxes. Attatchments are possible with negative integers as well. Consider negative boxes, we denote a lack. -4 -> concept of needing 4 boxes. We can never make our way down to the concrete object box. But the relationship with concrete objects are still obvious. As we go higher and higher we are less able to associate with concrete objects and the relationship is less visible: say with some number q which is a quaternion for example. This is not so easily associated and we have less concrete experience with such a concept and so feel it to be less natural, where infact the positive integers are just as “fake” or “real” as the the quaternions. We are used to handling integers, the path from the positive integer concept to a concrete object is quite simple, creating an illusionary concept of concreteness. The more complex our numbers the less we take them for granted and the more distrustful we are (their path to experience is too complicated), conversly for simple numbers like the positive integers we have little difficulty, in fact so little it may be considered that we cannot dissasociate positive integers from objects. This causes problems on what a number is and creates misconceptions on what a number may be and in the future resulting in us being mistrustful to treat perfectly valid numbers as numbers.

General sketch on how to construct the natural numbers

One way to construct the natural numbers due to Von Neuman is to use set theoretic formulations to define them. I go into it very informally. Consider the empty set ∅ (a set is an aggregration/conglomeration of a collection of objects. A pack is to set as a set’s members is to wolves, a pack is a conglemeration of wolves). The empty set has no members. It is itself a an existing thing but has nothing whatsoever as its contents. Basically a collection of pure nothings. So we take the empty set and from there make a set with that as its member. We then make another set that has the empty set and the set(s) we have made as its members. We do this ad infinitum. This construction has that each stage in our constructing, the current set in question has all the previous sets as its members.

So we have ∅ -> {∅} -> {∅ , {∅}} -> {∅ ,{∅}, {∅ , {∅}}} -> …

The Set (as an implentation of the peano axioms which tell us what it takes to be considered the natural numbers) which contains all these sets is equivalent to isomorphism to (basically the same as) the natural numbers. Yes that is:
∅ = 0
{∅} = 1
{∅ , {∅}} = 2
{∅ ,{∅}, {∅ , {∅}}} = 3

This has the interesting property that the number 52 is inside 100, the number 52 is contained in 100. In fact the number 100 contains all the numbers previous to it inside it (as members). The Natural numbers, in essence, under this method is basically made out of nothing. We just have collections of empty aggregrations. That is our natural numbers that are so real and obvious.

As a final excercise consider the Real Number Line. Try and point out the location of π on it. We may get arbitrarily close to it, zoom in closer and closer but we will never arrive at it or equivallently, we do so at infinity. How is that “real” number any more real than the square root of -1?