0

This might be quite a naïve question, but I seem to be unable to find a good answer.

The set-valued functional $$ F(X) = (X \to X) \cup \{ \bot \} $$ is not monotonic: $F(\{t\}) = \{\bot,\mathrm{id}_{ \{ t \} }\} \not \subseteq F(\{t,f\}) = \{ \bot,\mathrm{id}_{\{t,f\}},\mathrm{not} \}$ if you represent $A \to B \subseteq A \times B$ as its graph (note that $\mathrm{id}_{\{t\}} \neq \mathrm{id}_{\{t,f\}}$; the former has a graph of one element while the latter has a graph with two elements), so we can't use the usual fixpoint theorems.

How can we show in the simplest possible terms (preferrably by counter-example) that a (the least) fixed-point of $F$ does in fact not exist? (Which is the result I would expect, but I'm prepared to be surprised.)

Lemmon
  • 1,234
Sebastian Graf
  • 101

1 Answers1

0

In hindsight this is probably somewhat obvious to an undergrad mathematician, but it is of vital importance to programming language semanticists, so here it goes:

Suppose that $μF$ is the fixed-point of $F$. Then there must be an injection $fun : (μF \to μF) \to μF$. On the other hand, $μF$ contains at least two elements (e.g., $\bot, (λ\_.\bot)$), so the cardinality of $μF \to μF = μF^{μF}$ is at least the cardinality of $2^{μF}$, the set of two-valued functions on $μF$. But $2^{μF}$ is one-to-one with the powerset $\mathcal{P}(μF)$, and Cantor has proven that the latter has strictly larger cardinality than $μF$ and then so has $μF^{μF}$. That is in contradiction to the existence of the injection $fun$.

Sebastian Graf
  • 101