The stupidity and innumeracy of Americans, and in particular American fundamentalists, never ceases to astound me.

Recently on Yahoo, some bozo posted [something claiming that the bible was all correct][yahoo], and that genetics would show that bats were actually birds. But that’s not the real prize. The *real* prize of the discussion was in the ensuing thread.

A doubter posted the following question:

>please explain 1 kings 7.23 and how a circle can have a circumference of 30 of

>a unit and a radiius of 10 of a unit and i will become a christian

>

>23 And he made the Sea of cast bronze, ten cubits from one brim to the other;

>it was completely round. Its height was five cubits, and a line of thirty

>cubits measured its circumference. (1 Kings 7:23, NKJV)

And the answer is one of the all-time greats of moronic innumeracy:

>Very easy. You are talking about the value of Pi.

>That is actually 3 not 3.14…….

>The digits after the decimal forms a geometric series and

>it will converge to the value zero. So, 3.14…..=3.00=3.

>Nobody still calculated the precise value of Pi. In future

>they will and apply advenced Mathematics to prove the value of Pi=3.

[yahoo]: http://answers.yahoo.com/question/?qid=20060808164320AAl8z7K&r=w#EsArCTu7WTNaDSL.CVTGFHpKzx2nixwD70ICPWo2wTRcAQawQUIY

# Return of the Bible Code Bozos

Remember back in the end of june, when I [talked about these insane bozos][code] who were [predicting that a nuclear bomb would be blown up in the UN plaza?][firsttime] And they were on their fourth prediction about when this would happen? And how each time they blew it, [they came up with an excuse for why they were wrong?][update]

I thought it would be fun to take a look back at them, and see what they’re up to six weeks later. Naturally, [they’re still at it.][bozos] They’ve updated their prediction 5 more times now.

But there are a couple of really amusing things about what they’re up to now.

First, they’ve declared victory:

>We correctly predicted that the UN would lose its headship in 2006Tammuz (this

>being the 2nd head of the image of the Beast of Revelation 13) which gets a

>death stroke but then recovers. It lost its head on 2006July12 when Israel

>invaded Lebanon without a UN mandate. The UN lost credibility and lost control >for a month. It lost headship over Israel for one month. But the image of the

>Beast does not lose two heads, it only loses one head. Each of the 7 heads of

>the image of the UN Beast stands for one month of military headship over the

>governments of the world, just as the 7 heads of the UN Beast itself each stand

>for one year of military headship over the governments of the world. So we knew

>it had to regain headship this month and it did by virtue of the multilaterally

>agreed UN Security Council ceasefire resolution of Friday 2006August11. Now the

>UN will declare Peace and Security and then sudden destruction will befall them

>according to 1 Thessalonians 5:3. So please leave NYC for the sabbath!!!

And second, they’ve worked *their errors* into their code. That is, they’re now saying that their bible code *predicts* that they’d get it wrong seven times, so that their *eighth* prediction will be right. But they’ve made 9 predictions! So what to do? Well, hedge of course. You see, only the *correct* incorrect predictions count. So they have an explanation for why *some* of the incorrect predictions were *correct* incorrect predictions, and some were *incorrect* incorrect predictions.

>On April 29th we started predicting dates for a terrorist Nuclear Bomb at the

>UN in midtown. After making several mistakes we realised that 1 Kings 18:43

>declared we would get it right at the 8th attempt (Since Elijah asked his

>attendant to go and look for a man made mushroom cloud 7 times after the first

>no show, making 8 attempts in all). The trouble is that we have found it hard

>to decide just what a valid attempt is. Here are all the incorrect dates we

>have so far proposed…

>

>2006Iyyar21 (May 19/20) [7 days after 2006Iyyar14]

>2006Iyyar28 (May 26/27) [7 days after first mistaken date]

>2006Iyyar11 (June 8/9) [First day of the 2,000 pigs of Mark 5 incorrectly calculated]

>2006Sivan12 (June 9/10) [First day of the 2,000 pigs of Mark 5 correctly calculated but misinterpreted]

>2006Tammuz2/3 (June30-July2) [7th sabbath after first mistaken date/7th sabbath omitting 2006Sivan5]

>2006Tammuz4-6 (July2 – July 4) [7th sabbath day when we asked people to lookout]

>2006Tammuz28/29 (July 25 – 27) [Assumed contest began on 911]

>2006Ab3/4 (July 30 – August 1) [Assumed second ‘day’ of contest began when wheat went limit up in Chicago]

>2006Ab8 (August 4/5) [Assumed second ‘day’ of contest began on non BLC day of 2006Adar28 so that 1750th day is sabbath]

>

>What we now propose is…

>

>2006Ab15 (August 11/12) [7th sabbath lookout period after first mistake]

>

>So one could say you have had 9 attempts, you screwed up each time, give up and

>try doing something less dramatic! But although our repeated failures would at

>first sight take more and more credibility away from our work, the world

>security situation is for a fact moving in a direction that lends more and more

>credibility to our work. We started behaving as prophets of Doom for the UN and

>for Manhattan on April 29th 2006, when we proposed 2006Iyyar11 (June 8/9) as

>the date of the first nuclear terrorist attack. At that time the following

>global security situation existed…

Gotta love it, eh?

I’ll give ’em credit for their persistence, if not for their intelligence, or their sanity, or their rationality, or even their theology.

[update]: http://scienceblogs.com/goodmath/2006/07/an_update_on_the_bible_code_bo.php

[code]: http://scienceblogs.com/goodmath/2006/07/bible_code_bozos.php

[firsttime]: http://scienceblogs.com/goodmath/2006/06/good_math_bad_math_might_be_in.php

[bozos]: http://www.truebiblecode.com/index.html

# A Brilliant φ link

In the comments onmy post about φ, Polymath, (whose [blog][polymath] is well worth checking out) provided a really spectacular [link involving φ][desert]. It’s an excerpt from a book called “[Mathematical Gems 2][gems]”, showing a problem that came from John Conway, called the “Sending Scouts into the Desert” problem.

The problem is:

Suppose you’re given a checkerboard with all of the squares on the bottom filled. You’re allowed to do standard checks jumps (jump over a man and remove it), but you can’t jump diagonally, only up, left, or right. How far *up* can you get a man? How many men do you need to move to get that far?

To get to the first row above your men, you need to jump one man. To get two rows, you need to jump four men; three rows, you’ll need 8 men; four rows, you’ll need 20 men. How about five rows?

You *can’t* get five rows doing up and sideways jumps. Even if you had an infinitely wide checkerboard, with as many full rows of mens as you want.

The proof, along with a nice Java applet to let you try the solvable ones, is at the link. And φ is an inextricable part of the proof!

[polymath]: http://polymathematics.typepad.com/

[desert]: http://www.cut-the-knot.org/proofs/checker.shtml

[gems]: http://www.amazon.com/gp/redirect.html?link_code=ur2&tag=goodmathbadma-20&camp=1789&creative=9325&location=%2Fgp%2Fproduct%2F0883853027%2Fsr%3D8-2%2Fqid%3D1155392829%2Fref%3Dpd_bbs_2%3Fie%3DUTF8

# Friday Pathological Programming: Unlambda, or Programming Without Variables

Todays tasty treat: a variable-free nearly-pure functional programming language: Unlambda.

Unlambda is based on the SKI combinator calculus. The [SKI calculus][ski] is a way of writing lambda calculus without variables, and without lambda. It’s based on three combinators: S, K, and I:

1. S = λ x y z . x z (y z)

2. K = λ x y . x

3. I = λ x . x

Given only S and K, you can actually write *any* lambda calculus expression – and therefore, you can write any computable function using nothing but S and K. I is often added for convenience; it’s just a shorthand for “SKK”.

You can do recursion in SKI; the Y combinator of lambda calculus is:

Y = S S K (S (K (S S (S (S S K)))) K)

Unlambda is based on SKI; but it extends it with a few additional kinds of sugar to make things easier to write. (Nothing makes Unlambda easier to *read*!) The basic idea is that *everything* in unlambda is a function; and in particular, everything is a function that takes a *single* variable: you don’t need more than one parameter, because you can always using [currying][curry] to express any multiparameter function as a series of single-parameter functions.

(As a refresher, if you have a two-parameter function in lambda calculus, like “λ x y . x + y”; *currying* is translating it into a one parameter function that returns a one parameter function: “λ x .(λ y. x + y)”.)

There are eight basic instructions in Unlambda:

1. ““”` : the application operator. “`’AB`” applies the function `A` to the parameter `B`. You can think of this as being something like the “(” in Lisp; there is no close paren because since every function takes only one parameter, there is no *need* for a close paren. And hey, adding a syntactically unnecessary close paren would only make the code easier to read, and we can’t have that!

2. “`k`” : the K combinator.

3. “`s`” : the S combinator.

4. “`i`” : the I combinator.

5. “`v`” : a “drop” combinator: takes a parameter, discards it, and returns “`v`”

6. “`d`” : the “delay” operator; a way of doing *lazy evaluation* in Unlambda. Unlambda normally evaluates the argument before it

applies a function. `’dA` is the same thing as `A`, except that `A` isn’t evaluated until “`’dA`” is applied to something else.

7. “`c`” : the “call-with-current-continuation” combinator. This is equivalent to [“call/cc”][callcc] in Scheme. What it does is call some function with the current state of the computation captured as a function as its parameter. What this means is that “`’cAB`” calls “`A`”. “`A`” receives the value “`cAB`” as a parameter; during A, it can return a value, *or* it can call the continuation, which will evaluate “`cAB`” again. So this is the function-based equivalent of a loop. “c” turns the “loop body” into a function; so at the end of the loop, you re-invoke the continuation with a new parameter to run the next iteration.

8. “`.`” : The “.” operator is actually a meta-operator. “`.x`” is a function which returns its parameter, *and* prints the character “x”.

9. “`r`” is a shorthand for “`.CR`”, where CR is the carriage return character.

And that is it. The entire language.

Note that there are no numbers! We need to build numbers using church numerals.

* The church numeral “0” is “λ f. (λ x . x)”. In Unlambda, that’s “`’ki`”.

* The church numeral “1” is “λ f . (λ x . f x)”; in unlambda, that’s “`i`”.

* The church numeral “2” is “λ f . (λ x. f f x)”; or “`”s”s’kski`”.

* The church numeral “3” is “λ f . (λ x . f f f x)”; or “`”s”s’ksk”s”s’kski`”.

* And so on.. Just keep appending “`”s”skski`” for each successive number.

So… On to a couple of programs!

Hello world in Unlambda is:

`r“““““`.H.e.l.l.o. .w.o.r.l.di

It’s pretty straightforward. It’s actually sort of easier to understand if you look from right to left. The “`.H.e.l.l.o…`” is basically a series of “`i`” combinators, which print out the characters of hello world. The trailing “`i`” is there because “`.d`” needs a parameter in order to do anything. And the list of “`’`”s at the beginning are there to make the “.” functions be applied. Finally, apply “`’r`” to the whole thing – which prints a newline at the end.

Next, a counter: starts with “N=1”; print “N” asterisks, add one, and then repeat.

“r`ci“s`k`c“s“s`ksk`kr.*

If you look at it, you can see the number pattern in there; “`”s”s’ksk`”. That fragment is an SKI function to add one. You capture a continuation for the main iteration; run “`i”s’k’cN`”; that’s a fragment that adds “1” to N, and then prints N. Since you’ve captured the continuation, you can re-invoke it on 1+n; the rest captures *another* continuation which is the inner loop for printing “*”s; it does that, and then it invokes the out continuation to go back and do it for “N+1”.

One last, which I’ll leave for you to trace through yourself: this one generates the fibonacci sequence; and for each element of it, it prints out the numbers using a line of asterisks containing “N” asterisks for the number “N”:

“`s“s“sii`ki

`k.*“s“s`ks

“s`k`s`ks“s“s`ks“s`k`s`kr“s`k`sikk

`k“s`ksk

I’ll also point out that there are a ton of variants on Unlambda, ranging from the really interesting ([LazyK][lazyk]) to the bizzarely minimal ([Iota][iota]) to the downright goofy ([Jot][jot]).

[callcc]: http://community.schemewiki.org/?call-with-current-continuation

[ski]: http://goodmath.blogspot.com/2006/05/from-lambda-calculus-to-combinator.html

[curry]: http://goodmath.blogspot.com/2006/05/my-favorite-calculus-lambda-part-1.html

[iota]: http://ling.ucsd.edu/~barker/Iota/

[lazyk]: http://homepages.cwi.nl/~tromp/cl/lazy-k.html

[jot]: http://ling.ucsd.edu/~barker/Iota/#Goedel

# From Lambda Calculus to Cartesian Closed Categories

This is one of the last posts in my series on category theory; and it’s a two parter. What I’m going to do in these two posts is show the correspondence between lambda calculus and the [cartesian closed categories][ccc]. If you’re not familiar with lambda calculus, you can take a look at my series of articles on it [here][lambda]. You might also want to follow the CCC link above, to remind yourself about the CCCs. (The short refresher is: a CCC is a category that has an exponent and a product, and is closed over both. The product is an abstract version of cartesian set product; the exponent is an abstraction of the idea of a function, with an “eval” arrow that does function evaluation.)

Today I’m going to show you one half of the correspondence: how the lambda-theory of any simply typed lambda calculus can be mapped onto a CCC. Tomorrow, I’ll show the other direction: how an arbitrary CCC can be mapped onto a lambda-theory.

First, let’s define the term “lambda theory”. In the simply typed lambda calculus, we always have a set of *base types* – the types of simple atomic values that can appear in lambda expressions. A *lambda theory* is a simply typed lambda calculus, plus a set of additional rules that define equivalences over the base types.

So, for example, if one of the base types of a lambda calculus was the natural numbers, the lambda theory would need to include rules to define equality over the natural numbers:

1. x = y if x=0 and y=0; and

2. x = y if x=s(x’) and y=s(y’) and x’ = y’

So. Suppose we have a lambda-theory **L**. We can construct a corresponding category C(**L**). The objects in C(**L**) are the *types* in **L**. The arrows in C(**L**) correspond to *families* of expressions in **L**; an arrow f : A → B corresponds to the set of expressions of type B that contain a single *free* variable of type A.

The *semantics* of the lambda-theory can be defined by a *functor*; in particular, a *cartesian closed* functor F that maps from C(**L**) to the closed cartesian category of Sets. (It’s worth noting that this is completely equivalent to the normal Kripke semantics for lambda calculus; but when you get into more complex lambda calculi, like Hindley-Milner variants, this categorical formulation is *much* simpler.)

We describe how we build the category for the lambda theory in terms of a CCC using something called an *interpretation function*. It’s really just a notation that allows us to describe the translation recursively. The interpretation function is written using brackets: [A] is the categorical interpretation of the type A from lambda calculus.

So, first, we define an object for each type in **L**, including “unit”, which is a special distinguished value used for an expression that doesn’t return anything:

* ∀ A ∈ basetypes(**L**), [A] = A_{C} ∈ C(**L**)

* [unit] = 1_{C}

Next, we need to define the typing rules for complex types:

* [ A × B ] = [A] × [B]

* [ A → B ] = [B]^{[A]}

Now for the really interesting part. We need to look at type derivations – that is, the type inference rules of the lambda calculus – to show how to do the correspondences between more complicated expressions. Type derivations are done with a *context* containing a set of *type judgements*. Each type judgement assigns a type to a lambda term. We write type contexts as capital greek letters like Γ. There are two translation rules for contexts:

* [∅] = 1_{C}

* [Γ, x : A] = [Γ] × [A]

We also need to describe what to do with the values of the primitive types:

* For each value v : A, there is an arrow v : 1 → A_{C}.

And now the rest of the rules. Each of these is of the form [Γ :- x : A] = arrow, where we’re saying that Γ entails the type judgement “x : A”. What it means is the object corresponding to the type information covering a type inference for an expression corresponds to the arrow in C(**L**).

* [Γ :- unit : Unit] = ! : [Γ] → [Unit] *(A unit expression is a special arrow “!” to the Unit object)*

* [Γ :- a : A_{C}] = a º ! : [Γ] → [A_{C}] *(A simple value expression is an arrow composing with ! to form an arrow from Γ to the type object of Cs type.)*

* [Γ x : A :- x : A] = π_{2} : ([Γ ] × [A]) → [A] *(A term which is a free variable of type A is an arrow from the product of Γ and the type object A to A; That is, an unknown value of type A is some arrow whose start point will be inferred by the continued interpretation of gamma, and which ends at A. So this is going to be an arrow from either unit or a parameter type to A – which is a statement that this expression evaluates to a value of type A.)*

* [Γ, x:A :- x’ : A’],x’ ≠ x = [Γ :- x’ : A’] º π_{1} where π_{1} : ([Γ] × [A]) → [A’]. *(If the type rules of Γ plus the judgement x : A gives us x’ : A’, then the term x’ : A’ is an arrow starting from the product of the interpretation of the full type context with A), and ending at A’. This is almost the same as the previous rule: it says that this will evaluate to an arrow for an expression that results in type A.)*

* [Γ :- λ x:A . M : A → B] = curry([Γ, x:A :- M:B]) : [Γ] → [B]^{[A]} *(A function typing rule: the function maps to an arrow from the type context to an exponential [B]^{[A]}, which is a function from A to B.)*

* [Γ :- (M M’) : B] = eval_{C,B} º ([Γ :- M : C → B], [Γ :- M’ : C]) : [Γ] → [B] *(A function evaluation rule; it takes the eval arrow from the categorical exponent, and uses it to evaluate out the function.)*

There are also two projection rules for the decomposing categorical products, but they’re basically more of the same, and this is already dense enough.

The intuition behind this is:

* *arrows* between types are families of values. A particular value is a particular arrow from unit to a type object.

* the categorical exponent *is* the same as a function type; a function *value* is an arrow to the type. Evaluating the function is using the categorical exponent’s eval arrow to “decompose” the exponent, and produce an arrow to the function’s result type; *that* arrow is the value that the function evaluates to.

And the semantics – called functorial semantics – maps from the objects in this category, C(**L**) to the category of Sets; function values to function arrows; type objects to sets; values to value objects and arrows. (For example, the natural number type would be an object like the NNO we showed yesterday in C(**L**), and the set of natural numbers is the sets category would be the target of the functor.)

Aside from the fact that this is actually a very clean way of defining the semantics of a not-so-simply typed lambda calculus, it’s also very useful in practice. There is a way of executing lambda calculus expressions as programs that is based on this, called the [Categorical Abstract Machine][cam]. The best performing lambda-calculus based programming language (and my personal all-time-favorite programming language), [Objective-CAML][caml] is based on the CAM. (CAML stands for categorical abstract machine language.)

[cam]: http://portal.acm.org/citation.cfm?id=34883&dl=ACM&coll=portal

[caml]: http://caml.inria.fr/

[lambda]: http://goodmath.blogspot.com/2006/06/lamda-calculus-index.html

[ccc]: http://scienceblogs.com/goodmath/2006/06/categories_products_exponentia_1.php

# Metamath and the Peano Induction Axiom

In email, someone pointed me at an automated proof system called [Metamath][metamath]. Metamath generates proofs of mathematical statements using ZF set theory. The proofs are actually relatively easy to follow, which is quite unusual for an automated theorem prover. I’ll definitely write more about Metamath some other time, but I thought it would be interesting today to point to [metamaths proof of the fifth axiom of Peano arithmetic][meta-peano], the principle of induction. Here’s a screenshot of the first 15 steps; following the link to see the whole thing.

[metamath]: http://us.metamath.org/mpegif/mmset.html#overview

[meta-peano]: http://us.metamath.org/mpegif/peano5.html

# More Loony Christian Math

Yesterday, I posted [this article][bozo] about the bozo who didn’t like his college calculus course because it wasn’t Christian enough. One of the commenters pointed out that there’s actually a site online where a college professor from a Christian college actually has [a collection of “devotionals”][devotional] to be presented along with the lecture in a basic calculus course.

They’re sufficiently insane that I have to quote a couple of them. No comment that I could possibly make could add anything to the sheer goofiness of these.

For the lesson on “Function Operations”:

>**God’s Surgical Improvements of our Actions**

>

>Genesis 50:15-21, Romans 3:9-10, 21-24

>

>One of the more horrible images in the book of Genesis is that of Joseph being

>sold by his brothers into slavery. This type of hate turned into evil act is a

>common occurrence in our world, too. In the Genesis situation, though, we are

>given the gift of 20-20 hindsight because we know the end of the story. God

>used the brothers’ evil action to prevent starvation of the descendants of

>Abraham. Joseph says, “You intended to harm me, but God intended it for

>good. ..” [Gen. 50:20] In the same way, God makes our unrighteous actions

>righteous through Christ. He surgically improves our actions to his own

>purpose.

>

>This idea of twisting something from one form into another is what happens when

>function operations work on elementary functions. You can start with two

>ordinary benign functions, the reciprocal function 1/x and sin(x), say, and put

>them together. Depending on how you put them together, you can create

>something interesting and easily understood, like sin(x)/x, or something with

>wild behavior, like sin(1/x). Either way, you have twisted one object into

>something very different.

For the lesson on the Limit definition of the derivative:

>**Secant Lines and Sanctification**

>

>Ps. 119:33-40

>In differential calculus we study how a slope of a linear function can be

>generalized to the slope of a function whose graph is curved, creating the

>derivative of the original function. The definition of derivative uses a

>sequence of lines (secant lines) drawn through two points on a function that

>are approaching each other and a single point on the function curve. The

>derivative value or tangent line slope is defined to be the limiting slope

>value of this sequence of secant lines. (See the figures below.)

>

> Figure 1 : Secant line between 1 and 1.8

> Figure 2 : Secant line between 1 and 1.5

> Figure 3: Tangent line to f at x=1

>

>Once a person has been called to be a Christian, we are redeemed by Christ but

>not released from following the law of God. We are justified once but continue

>with the process of sanctification for the remainder of our lives. This

>sanctification process is like the limit process of the secant lines

>approaching the tangent line. There is one distinction between the concepts of

>sanctification and secant line limits, however. In the mathematical contexts,

>we accept results that are “sufficiently close,” results that are in an

>epsilon-neighborhood of the desired quantity. While in our quest for

>perfection, the “better” we get the further we realize we are from satisfying

>all aspects of the law.

Ok, just one more. This one just about had me rolling on the floor! For the lesson on the chain rule:

>**Chain Reactions**

>

> 1 Corin 5:16-21

>

>Once students have seen the chain rule for differentiation of composed

>functions, it is natural to extend the chain rule to nested functions, where

>there is more than two functions that are composed. Fun problems to

>investigate are ones that are repeated applications of the same function. Try

>differentiating tan(tan(tan(tan(tan x)))) or ln(ln(ln(ln(ln(ln x))))), for

>example. Working your way from the outside to the inside yields a derivative

>which is product chain of related functions.

>

>In a similar way, when we interact with other people there is a chain reaction

>to our behavior. Most people believe that abused children are more likely to

>become abusers themselves someday, for example. Less dramatic behavior also

>can have a reaction that extends beyond the initial engagement. A popular

>Warner Brothers film of 2000 “Pay it Forward” (based on a novel with the same

>name by Catherine Ryan Hyde) depicts how a chain of reactions to an initial act

>of kindness can change an entire community. Christians need to be specially

>mindful of this chain reaction, since we are ambassadors for Christ. Our

>verbal and nonverbal witness can yield unexpected results, especially under the

>influence of the Holy Spirit.

This, apparently, is how “real” Christians are supposed to teach math classes. I seriously wonder how they have time to actually cover the *math* in class if they spend time on this gibberish!

[bozo]: http://scienceblogs.com/goodmath/2006/08/math_is_bad_because_it_isnt_ch.php

[devotional]: http://www.trnty.edu/faculty/robbert/SRobbertWebFolder/ChristianityMath/Calculus.html#Chain

# Categorical Numbers

Sorry for the delay in the category theory articles. I’ve been busy with work, and haven’t had time to do the research to be able to properly write up the last major topic that I plan to cover in cat theory. While doing my research on closed cartesian categories and lambda calculus, I came across this little tidbit that I hadn’t seen before, and I thought it would be worth taking a brief diversion to look at.

Category theory is sufficiently powerful that you can build all of mathematics from it. This is something that we’ve known for a long time. But it’s not really the easiest thing to demonstrate.

But then, I came across this lovely little article on wikipedia. It turns out that you can [build the natural numbers entirely in terms of categories][wikipedia] in a beautifully simple way.

Before we dive into categorical numbers, let’s take a moment to remember what we really mean by natural numbers.

Peano Arithmetic

——————

The meanings of natural numbers are normally defined in terms of what we call *Peano arithmetic*. Peano arithmetic defines the natural numbers, **N** in terms of five fundamental axioms:

1. 0 ∈ **N** (0 is a natural number.)

2. ∀ a ∈ **N** ∃ a’=s(n), a’ ∈ **N**. (Every natural number a has a successor, s(a))

3. ¬ ∃ a ∈ **N** : s(a)=0. (No natural number has 0 as its successor.)

4. ∀ a,b ∈ **N**: s(a)=s(b) ⇒ a=b. (Each number has a unique successor.)

5. (P(0) ∧ ∀ a : P(a) ⇒ P(s(a))) ⇒ ∀ b ∈ **N** : P(b). (If a property P is true for 0; and it can be shown that for any number a, if it’s true for a, then it’s true for b, then that means that it’s true for all natural numbers. This is the *axiom of induction*.)

To get to arithmetic, we need to add two operations: addition and multiplication.

We can define addition recursively quite easily:

1. ∀ x ∈ **N**: x+0 = x

2. ∀ x,y ∈ **N**: s(x)+y=x+s(y)

And once we have addition, we can do multiplication:

1. ∀ x ∈ **N**: x * 0 = 0 ∧ 0 * x = 0

2. ∀ x ∈ **N**: 1 * x = x

3. ∀ x,y ∈ **N**: s(x)*y = (x*y) + y

To sum up: Peano arithmetic is based on a definition of the natural numbers in terms of five fundamental properties, called the Peano axioms, built on “0”, a successor function, and induction. If we have those five properties, we can define addition and multiplication; and given those, we have the ability to build up arbitrary functions, sets, and the other fundamentals of mathematics in terms of the natural numbers.

Peano Naturals and Categories

———————————

The peano axioms can be captured in a category diagram for a relatively simple object called a *natural number object (NNO)*. A natural number object can exist in many categories: basically any category with a terminal object *can* have NNOs. Any closed cartesian category *does* have an NNO.

There are two alternate constructions; a general construct that works for all NNO-containing categories; and a more specific one for closed cartesian categories. (You can show that they are ultimately the same in a CCC.)

I actually think that the general one is easier to understand, so that’s what I’ll describe. This is basically a construction that captures the ideas of successor and recursion.

Given a category C with a terminal object **1**. A *natural number object* is an object *N* with two arrows z : 1 → *N*, and s : *N* → *N*, where z and s have the following property.

(∀ a ∈ Obj(C), (q : 1 → a, f : a → a) ∈ Arrows(C)) : u º z = q ∧ u º s = f º u.

That statement means the same thing as saying that the following diagram commutes:

Let’s just walk through that a bit. Think of the object **N** as a set. “s” is successor. So S is an arrow from *N* to *N* that maps each number to its successor. *N* is “rooted” by the terminal object; that gives it its basic structure. The “z” arrow from the terminal object maps to the zero value in *N*. So we’ve got an arrow that selects zero; and we’ve got an arrow that defines the successor.

Think of “q” as a predicate, and “u” as a statement that a value in *N* satisfies the predicate.

So u º z, that is the path from 1 to a by stepping through z and u is a statement that the predicate “q” is true for z (zero); because composing u (the number I’m composed with satisfies q) and z (the number zero) gives us “q” (zero satifies q).

Now the induction rule part. *N* maps to *N* by s – that’s saying that s is an arrow from a number in *N* to its successor. If you have an arrow composition that says “q is true for n”, then f can be composed onto that giving you “q is true for n + 1”.

If for all q, u is unique – that is, there is only *one* mapping where induction works; then you’ve got a categorical structure that satisfies the Peano axioms.

[wikipedia]: http://en.wikipedia.org/wiki/Natural_number_object

# Math is Bad, Because it isn't Christian!

By way of Pharyngula, I saw something that I simply had to repeat here.

Every august, James Kennedy – a thoroughly repulsive ultra-fundy preacher from Coral Ridge Ministries – runs a conference called “Reclaiming America for Christ”. At this years conference, he featured a speech by Paul Jehle about “Evaluating your Philosophy of Education”.

Jehle is… umm… how do we say this politely?….

Ah, screw it. Jehle is a fucking frothing at the mouth nutjob lunatic asshole.

His basic argument – the argument that he *expects people to take seriously* – is that *everything* is either christian or non-christian. And if it’s non-christian, then christians shouldn’t look at it, listen to it, or study it. And you can’t *ever* make anything that started out non-christian christian.

How far does he go with this? Pretty damned far. Right into the domain of this here blog. In his talk, he uses the following story as an example:

>I was taking calculus. I was a mathematics major and I was at a Christian

>college that was called Christian, but was not Christian….

>

>I asked a question to my calculus professor: “What makes this course distinctly

>Christian?” He stopped. He said no one has ever asked that question before…

>

>He said, “Okay, I’m a Christian; you’re a Christian.”

>

>I said, “That’s not what I asked! What makes this calculus course distinctly

>Christian? What makes this different from the local secular university? Are we

>using the same text? Yes. Are you teaching it the same way? Yes. Then why is

>this called a Christian college and that one a non-Christian college?”

Yeah. Seriously. **Math is Bad**, because it’s *not explicitly christian*. I mean, it uses *zero*, which was invented by a *hindu*, and brought to europe by *muslims*. Algebra was invented by muslims! The word “algorithm” comes from the name of a *muslim* mathematician!

Uh-oh… I just realized that the alleged “Doctor” Jehle has a very serious problem. The way that we geeks heard his talk to write about it is because it was *digitized* – using a thoroughly non-christian technology – and posted on the *internet*, which is built using those non-christian *algorithms*. And to quite Jehle himself:

>But the issue is you cannot combine something by its nature which is pagan and

>built on humanistic principles and make it Christian by a magic wand.

So the internet, and computers, and digital recording, and the data compression that makes streaming audio work – they’re *non-christian*. And you cannot combine something non-Christian with something Christian.

# φ, the Golden Ratio

Lots of folks have been asking me to write about φ, the golden ratio. I’m finally giving up and doing it. I’m not a big fan of φ. It’s a number

which has been adopted by all sorts of flakes and crazies, and there are alleged sightings of it in all sorts of strange places that are simply *not* real. For example, pyramid loons claim that the great pyramids in Egypt have proportions that come from φ – but they don’t. Animal mystics claim that the ratio of drones to larvae in a beehive is approximately φ – but it isn’t.

But it is an interesting number. My own personal reason for thinking it’s cool is representational: if you write φ as a continued fraction, it’s [1;1,1,1,1…]; and if you write it as a continued square root, it’s 1 + sqrt(1+sqrt(1+sqrt(1+sqrt(1…)))).

What is φ?

—————–

φ is the value so-called “golden ratio”: it’s the number that is a solution for the equation (a+b)/a = (a/b). (1+sqrt(5))/2. It’s the ratio where if you take a rectangle where the ratio of the length of the sides is 1:φ, then if you remove the largest possible square from it, you’ll get another rectangle whose sides have the ration φ:1. If you take the largest square from that, you’ll get a rectangle whose sides have the ratio 1:φ. And so on:

Allegedly, it’s the proportion of sides of a rectangle that produce the most aesthetically beautiful appearance. I’m not enough of a visual artist to judge that, so I’ve always just taken that on faith. But it *does* shows up in many places in geometry. For example, if you draw a five-pointed star, the ratio of the length of one of the point-to-point lines of the star to the length of the sides of the pentagon inside the star are φ:1:

φ is also related to the fibonacci series. In case you don’t remember, the fibonacci series is the set of numbers where each number in the series is the sum of the two previous: 1,1,2,3,5,8,13,… If Fib(n) is the *n*th number in the series, you can compute it as:

History