Scott Induction

Scott induction packages together some reasoning that we can do with fixed points. Recall:

Kleene fixed-point theorem

Given a domain $D$, a continuous function $f$ has a least fixed point, which we denote $\text{fix}(f):={⨆}_{n\ge 0}{f}^n(\perp ).$

Link to original

So take $D$ and $f$ as above. Take $S\subseteq D$, or equivalently some predicate $\Phi$ on $D$. If S respects:

• $\perp$ (base case)
• $f$ (inductive step)
• chains (closure)

then $\text{fix}(f)\in S$. written out more explicitly:

• $\perp \in S$
• $f(S)\subseteq S$
• $⨆s_n\in S$