Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
@user: I tried to format it. \meet seems to be giving error. Please replace with what you intended. – Aryabhata Jan 2 '11 at 19:24
shouldn't the meet be a join? – Yuval Filmus Jan 2 '11 at 19:47
Yes you are right , I changed it to join operator. @Moron thanks for formatting the post. I will take care of it when posting next time. – chinu Jan 3 '11 at 5:05
up vote 8 down vote accepted

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.

share|cite|improve this answer

See this.

share|cite|improve this answer
Thanks for the link. The paper doesn't address the sense in which the original proof is not constructive. – Andrés E. Caicedo Jan 2 '11 at 20:08

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.