On fixed-point theorems in synthetic computability

I forgot to record the fact that already two years ago I wrote a paper on Lawvere's fixed-point theorem in synthetic computability:

Andrej Bauer: On fixed-point theorems in synthetic computability. Tbilisi Mathematical Journal, Volume 10: Issue 3, pp. 167–181.

It was a special issue in honor of Professors Peter J. Freyd and F. William Lawvere on the occasion of their 80th birthdays.

Lawvere's paper "Diagonal arguments and cartesian closed categories proves a beautifully simple fixed point theorem.

Theorem: (Lawvere) If e:A→BAe:A→BA is a surjection then every f:B→Bf:B→B has a fixed point.

Proof. Because ee is a surjection, there is a∈Aa∈A such that e(a)=λx:A.f(e(x)(x))e(a)=λx:A.f(e(x)(x)), but then e(a)(a)=f(e(a)(a)e(a)(a)=f(e(a)(a). □◻

Lawvere's original version is a bit more general, but the one given here makes is very clear that Lawvere's fixed point theorem is the diagonal argument in crystallized form. Indeed, the contrapositive form of the theorem, namely

Corollary: If f:B→Bf:B→B has no fixed point then there is no surjection e:A→BAe:A→BA.

immediately implies a number of famous theorems that rely on the diagonal argument. For example, there can be no surjection A→{0,1}AA→{0,1}A because the map x↦1−xx↦1−x has no fixed point in {0,1}{0,1} -- and that is Cantors' theorem.

It not easy to find non-trivial instances to which Lawvere's theorem applies. Indeed, if excluded middle holds, then having a surjection e:A→BAe:A→BA implies that BB is the singleton. We should look for interesting instances in categories other than classical sets. In my paper I do so: I show that countably based ωω-cpos in the effective topos are countable and closed under countable products, which gives us a rich supply of objects BB such that there is a surjection N→BNN→BN.

Enjoy the paper!