The names of birds, part 3

In the autumn of last year my friend Joan and I went on a little trip up to the Skagit valley north of Seattle to photograph birds of prey; I managed to get a blurry but recognizable shot of this charming little kestrel looking for field mice. It was easily identifiable in the field because kestrels are one of the very few birds of prey that can briefly hover while hunting, almost like a hummingbird.

Well, back to combinatory logic and some puzzles from To Mock a Mockingbird.

We’ve said that if there are birds x and y such that xy=y, then x is fond of y, and y is a fixpoint of x. Smullyan goes on to say that if there are birds x and y such that xz=y for every z in the forest, then x is not just fond of y, it is fixated on y.

The kestrel, K, is an interesting bird. When you call the name of any bird x to it, it calls back the name of a bird in the forest that is fixated on x. That is, the kestrel obeys the identity Kxy=x for all birds x and y in the forest. (Recall from part one that Kxy means (Kx)y, not K(xy).)

Suppose there is a forest which contains a kestrel and moreover in this particular forest K is fond of itself; that is KK=K. Can you prove that a kestrel that is fond of itself is both (1) extremely egocentric, and (2) lonely? Give it a try, and then scroll down.

_{I need a longer lens! This is at the edge of what my little 70-300 zoom can handle.}

(1) A bird which is fond of itself is already probably pretty egocentric. Kx gives the name of a bird which is fixated on x, so KK gives the name of a bird which is fixated on K. But KK=K, so K is the name of a bird that is fixated on K. A bird which is fixated on itself is surely extremely egocentric!

(2) By definition (Kx)y=x for all x and y. Since in this forest K is fixated on K, Kx=K for all x. Therefore Ky=x for all x, y. But again Ky=K for all y so K=x for all x in the forest. Every bird in the forest is the kestrel, and therefore there is only one bird in the forest. No wonder an extremely egocentric kestrel is lonely!

Next time on FAIC: The starling!

3 thoughts on “The names of birds, part 3”

I’ve spent some time writing up each part in Coq, and I discovered the interesting property that a bird which is fond of itself and fixated on another bird (assuming they are all in the same forest) is in fact the other bird. This is a weaker property than loneliness, but it fell out of my proof for loneliness.

In short, the equality “k = b” holds by transitivity with “kk”; the two equations (a) “k = kk” and (b) “kk = b” only require that (a) k is fond of k and (b) k is fixated on b (to be sure, a stronger claim than “kk = b,” but one given by the egocentricity of a self-fond kestrel). No kestrel properties required.

That parenthetical took me some time to wrap my brain around: a self-fond kestrel k is egocentric as shown, but this implies that k is fixated on any bird b! Egocentricity gives “kb = k,” but replace “k is fixated with b” with “kb is fixated with b” which is equivalent to “k is a kestrel”!

https://github.com/benknoble/junk-drawer/blob/master/code/mockingbirds.v, esp. https://github.com/benknoble/junk-drawer/blob/aad6a93e52cf717b6d78a48f9c366402f70e329f/code/mockingbirds.v#L72

Reply ↓