Reference. Tarski’s Fixed Point Theorem* [harper-tarski-fixed-point-2025]

January 1, 2025
Harper, Robert
Carnegie Mellon University
file:///mnt/data/tarski.pdf

Backlinks

Definition. Tarski's Theorem [002b]

November 25, 2025

We define a set \(X\), let \(\mathcal L(X)\) be the complete lattice of all subsets of \(X\) ordered by inclusion. A function \(f: \mathcal L(X) \to \mathcal L(X)\) is said to be monotone in this instance if it preserves inclusion which is to say that the following holds: (1)

\[ A \subseteq B \subseteq X \implies f(A) \subseteq f(B) \]

Pre-and-post fixed point

November 25, 2025

For a monotone function \(f\) a pre-fixed point of \(f\) is a subset \(A \subseteq X\) such that \(f(A) \subseteq A\). Similarly, a post-fixed point of \(f\) is a subset \(B \subseteq X\) such that \(B \subseteq f(B)\).

Conceptually the idea here is that the prefixed points are those sets in \(X\) where the function \(f\) maps to at most all members in \(A\). Conversely, the post-fixed points represent the subset where at least all members of the set are mapped to by other members of the same set. Another way to describe it would be that the pre-fixed points represent a closed or under-approximation of the function \(f\) while the post-fixed points represent a consistent or over-approximation of the function.

A pre-fixed point of \(f\) is also said to be \(f\)-closed and a post-fixed point of \(f\) is said to be \(f\)-consistent.

A least pre-fixed point of a monotone \(f\) is the smallest subset \(A \subseteq X\) such that \(f(A) \subseteq A\), denoted by \(\mu f\). Similarly, a greatest post-fixed point of \(f\) is the largest subset \(B \subseteq X\) such that \(B \subseteq f(B)\), denoted by \(\nu f\).

Every monotone function \(f\) has a unique least pre-fixed point and a unique greatest post-fixed point given by the following equations:

\[ \begin {align*} \mu f & = \bigcap \{ A \subseteq X \mid f(A) \subseteq A \} \\ \nu f & = \bigcup \{ B \subseteq X \mid B \subseteq f(B) \} \end {align*} \]

Of note here is that the least pre-fixed point here corresponds to the closure of the function \(f\). That is to say that it is the smallest set which is closed under the function \(f\). Conversely, the greatest post-fixed point corresponds to the consistency of the function \(f\), being the largest set which is consistent with respect to \(f\).

Lambek's lemma

November 25, 2025

One thing we can observe is that \(\mu f\) is contained in all pre-fixed points of \(f\), by virtue of being the intersection, i.e. closure for all pre-fixed points. Furthermore, we have that \(\mu f\) is itself a pre-fixed point of \(f\)

\[ f(\mu f) \subseteq \mu f \]

and it is thereby the least pre-fixed point. To see this we note that if:

\[ f(A ) \subseteq A \to f(\mu f) \subseteq A \]

Explanation

November 25, 2025

So the idea here is again that since \(A\) is a pre-fixed point of \(f\), by definition we have that \(f(A) \subseteq A\). The implication here is that if we apply \(f\) to our closure, the resulting set must still be within \(A\) since again we definitionally cannot have that \(f\) maps outside \(A\) so even if we constrain ourselves to some smaller set \(\mu f\) it doesn't negate the fact that \(f\) still cannot map outside \(A\).

But by definition of \(\mu f\) we have that

\[ \mu f \subseteq A \]

Explanation

November 25, 2025

This is more or less just restating the definition of \(\mu f\) as the intersection of all pre-fixed points of \(f\), which includes \(A\).

Thus by monotonicity of \(f\) we have the following as required

\[ f(\mu f) \subseteq f(A) \subseteq A \]

Additionally we have

\[ f(f(\mu f)) \subseteq f(\mu f) \]

Which is to reiterate that \(f(\mu f)\) is itself a pre-fixed point of \(f\). Therefore, we have that

\[ \mu f \subseteq f(\mu f) \]

Explanation

November 25, 2025

What this says at a high level; or what it implies given the above condition; is that the application of the monotone operator to the closure set \(\mu f\) doesn't shrink the set any further, in other words its operation stabilizes at this set such that each member in this set maps precisely to some other member in the set not more (i.e. outside as that would mean it's not closed) and not less (as that would imply it's not minimal).

\[ f(\mu f) \subseteq \mu f \]

What this says at a high level; or what it implies given the above condition; is that the application of the monotone operator to the closure set \(\mu f\) doesn't shrink the set any further, in other words its operation stabilizes at this set such that each member in this set maps precisely to some other member in the set not more (i.e. outside as that would mean it's not closed) and not less (as that would imply it's not minimal). A question I had here was:

But why does this actually happen?

A nice perspective to have firstly is seeing the set \(\mu f\) here as a generating set for the function \(f\). In other words if we view the function \(f\) as a set of rules which generate new members in the set from existing members, then the closure \(\mu f\) represents the most precise set of members which can be generated by these rules without introducing any extraneous members.

The effect of this is that because the members in \(\mu f\) are precisely those which can be generated by the rules in \(f\), applying \(f\) to this set will simply regenerate the same members, hence why we have that \(\mu f \subseteq f(\mu f)\) since all the members in \(\mu f\) already correspond to members generated by the members of \(\mu f\) under the rules of \(f\)

Furthermore, since we are working in the context of a complete lattice, as we take the intersection of more and more closed subsets under \(f\) we eventually reach a point where if we take some further intersection (move down more) we end up losing the closed property, but if we move up (i.e. take the union of more closed sets) we end up introducing extraneous members which violate the minimalism property, hence the idea that we stabilize at this set i.e. we are a fixed point on the lattice under the operator.

The implication of this being that the closure \(\mu f\) is a fixed point of \(f\), and, because any fixed point is a pre-fixed point, it is the least pre-fixed point of \(f\). A dual argument shows that the greatest post-fixed point \(\nu f\) is also a fixed point of \(f\). This result is known as Lambek's lemma in Category theory.