Is the Knaster-Tarski Fixed Point Theorem constructive?

According to Tarski's Fixed Point Theorem, for a complete lattice $L$, and monotone function $f:L \rightarrow L$, the set of fixed points of $f$ forms complete lattice.

Definition of $lfp(f)$ and $gfp(f)$ is given in terms of set $\text{Red}(f)$ and $\text{Ext}(f)$. Where $\text{Red}(f)$ is set of all those points $l' \in L$, which satisfy $f(l') \le l'$. Similarly $\text{Ext}(f)$ is set of all those points $l'' \in L$, which satisfy $f(l'') \ge l''$.

$lfp(f) = \bigcap(\text{Red}(f))$ and $gfp(f) = \bigcup(\text{Ext}(f))$

I read somewhere that these definitions are not constructive in nature, so to reach least fixed point we try to find out least upper bound of the sequence $(f^n(\bot))_n$, i.e. $f(\bot) \sqcup f(f(\bot)) \sqcup f(f(f(\bot))) \dots$,

(Here $\bot$ is least element of lattice $L$ ).

Can someone please explain it further what do we mean by constructive definition here, and how these two definitions of $lfp(f)$ coincide?

Solution 1:

The first thing to know about the word "constructive" is that it means too many things. There are so many sorts of "constructive mathematics" that significant context is needed to tell which one is meant.

That being said, the clearest sense in which the definitions you have above are nonconstructive is that they are "impredicative". This means that, when you look at the definition $\operatorname{lfp}(f) = \bigcap \operatorname{Red}(f)$, you see that the element $\operatorname{lfp}(f)$ is already a member of $\operatorname{Red}(f)$. In ordinary mathematics as it is practiced, this is just a curiosity, but for a time there was concern about the impredicative definitions.

The first motivation for this concern was Russell's paradox: if we seek to define "the set of all sets that do not contain themselves", we see that the set we are defining is already a member of the collection of "all sets" that we quantify over, and moreover this impredicative definition leads to a paradox. This led Russell to be interested in predicativism (the program of developing mathematics without impredicative definitions. Later Weyl in Das Kontinuum showed that is is possible to develop a significant amount of mathematics in a predicative way; this work has been further extended and clarified by the reverse mathematics program of Friedman and Simpson.

One way to conceptualize the difference between predicative and impredicative definitions (not formal, but informative) is that impredicative definitions often "identify" something that already exists, while predicative definitions directly "construct" it. For example, you could define the supremum of a nonempty bounded set of real numbers as the least element of the set of all upper bounds - this impredicative definitions identifies which upper bound is the supremum, but it doesn't help you actually construct it. Or you could directly construct a Cauchy sequence whose limit you can prove is both an upper bound for the original set and a lower bound for the set of all upper bounds. This would give you a predicative definition of the supremum.

The way to build the Cauchy sequence is as follows. Suppose $A$ is a nonempty set with an upper bound $x_0 \not \in A$. Pick $y_0 \in A$. Now, by induction, assume $y_i, x_i$ are given with $y_i \in A$, $x_i \not \in A$, $y_i < x_i$. Let $z = (x_i + y_i)/2$. If $z \in A$ let $y_{i+1} = z$ and $x_{i+1} = x_i$. Otherwise let $y_{i+1} = y_i$ and $x_{i+1} = z$. Then the sequence $(x_i)$ is Cauchy, and you can prove its limit is the least upper bound of $A$. You can see that this took a lot more work than the impredicative definition of the supremum, but it also gives a lot more information: if you knew enough about the set $A$ you could use this procedure to actually approximate the supremum to any precision you like.

Similarly, there are two proofs of the Knaster–Tarski theorem. One is impredicative but otherwise easy, while the other is predicative but uses transfinite induction. There are many other mathematical objects that have the same pattern of two definitions. Another common one is the algebra of Borel sets on a topological space.

Solution 2:

See this.

Solution 3:

Carl is right in that there are many different schools of constructive mathematics. That said, the Knaster–Tarski theorem in the version you stated is true intuitionistically, i.e. valid in any topos.

The nice paper On the Bourbaki–Witt Principle in Toposes by Andrej Bauer and Peter LeFanu Lumsdaine gives an intuitionistic proof (it's really just the usual one) and also discusses the intuitionistic validity of several variants of the Knaster–Tarski theorem, including a variant where the fixpoint is attained as the supremum of the chain $(f^n(\bot))_n$. Don't let the word "topos" stop you, toposes don't appear until page 11.