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!

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

Nice analysis; I’ve been meaning to learn Coq and this seems like a good introduction.

Pingback: Dew Drop – February 2, 2023 (#3871) – Morning Dew by Alvin Ashcraft