Re:Category Theory, Syntactically (2016)
by ScottBurson on Thursday April 27, 2017 @06:11PM
(#14215214)
Fascinating! A couple of questions:
Are there any non-singleton sets with the fixpoint property?
> a ↦ f (e a a)
Don't you mean
a ↦ e a a
? Because later you expand (g a0) to (e a0 a0).
The key insight behind Lawvere's abstract framework to paradoxa is the the general existence of certain fixpoints.
Definition. We say that a set B has the fixpoint property if any function f:B→B has a fixpoint (i.e. f b = b for some b in B).
With this convenient definition, we are now ready to state and prove Lawvere's ridiculously simple and yet great theorem.
Theorem (Lawvere). If e:A→(A→B) is a surjective function, then B has the fixed point property.
The proof is quite easy. Let e:A→(A→B) be surjective. We have to show that B has the fixpoint property. That means for every f:B→B there is b∈B such that f(b)=b. Choose a function f:B→B and define the function g:A→B by setting
As e is surjective, there must be a0∈A such that But then immediately Hence g a0 is a fixpoint of f's.Now many/most paradoxa are special cases of Lawvere's theorem. But for each paradox, the specific functions involved are a bit different. Let's look at an example.
Theorem (Cantor). There is no surjection e:A→Pow(A).
To see why this is true, note that Pow(A) is isomorphic to A→Bool. But there is a function on Bool that has no fixpoints, for example negation ¬:Bool→Bool, contradicting Lawvere's theorem.
What is the intuition behind Lawvere's theorem? At first worrying about A→(A→Bool) is a bit surprising. What does that have to do with paradoxa and self-reference?Well, what does it mean that A can speak about itself? To approach an answer, we could maybe first ask a simpler question: what does it mean to speak about A? How about this for an answer: to speak about A means to say something about A's elements. What does it mean to say something about A's elements? Maybe stating whether any given element a∈A has a property of interest? But what's a property? Easy: a property of A's elements is a function
But we don't want just a fixed property, we want arbitrary properties. To do so, we have to consider the function space And how can we turn this into self-reference? What if each element a in A corresponded to a property over A? In other words, (with a lot of handwaving) self-reference means the existence of a surjective function The next step is to wonder: why Bool? Why not any old set? Note that Cantor's theorem continues to hold if we replace Bool with a larger set, but does not hold, if B in A→(A→B) has cardinality 1. What Bool and larger sets have in common is that we can rearrange them, i.e. there is a permuation that doesn't have a fixpoint.