(Co)-induction, fixpoints and inference systems

I'm learning about induction and co-induction. From what I know, given a set of judgments $$U$$ and an inference system $$\Phi \subseteq \wp(U) \times U$$, where $$(\left\{ h_1,\dots,h_n \right\}, c) \in \Phi$$ stands for the rule $$\frac{h_1 \quad \dots \quad h_{n}}{c}$$, we can define the function:

$$F_{\Phi}(X) = \left\{ c \mid \exists (H, c) \in \Phi \;.\; H \subseteq X \right\},$$

and the least fixpoint $$\mu F_{\Phi}$$ is the set of all judgments that have a finite proof in $$\Phi$$.

The induction principle states that $$F_{\Phi}(X) \subseteq X \Rightarrow \mu F_{\Phi} \subseteq X$$. It is a consequence of the Knaster-Tarski theorem, which requires that $$F_{\Phi}$$ be monotone.

However, not all inference systems seem to be monotone; they would be if they contained "identity" rules of the form $$(c,c)$$ for all $$c \in U$$. For instance, take $$U = \left\{ 0,1 \right\}$$ and $$\Phi = \left\{ \frac{}{0}, \frac{0}{1} \right\}$$: $$F_{\Phi}(\varnothing) = {0}$$ and $$F_{\Phi}(\{1\}) = \varnothing$$, so $$F_{\Phi}$$ is not monotone.

On the other hand, if an inference system has identity rules then co-induction is meaningless, since the greatest fixpoint of $$F_{\Phi}$$ is $$U$$ in that case.

There's clearly some flaw in my understanding, I would be grateful if somebody could point out my mistakes.

• $F_\Phi(\{1\}) = \{0, 1\}$ though!
– cody
Commented Nov 29, 2023 at 19:26
• @cody it's $\{0\}$ I think, still enough to be monotone... dumb mistake. I think this answers the question, thanks :)
– dalz
Commented Nov 29, 2023 at 21:47
• Right, sorry. Still a good question IMO.
– cody
Commented Nov 29, 2023 at 22:10

Intuitively, you can see that $$F_\Phi(X)$$ is monotone in $$X$$ by carefully looking at the body of the definition
$$\exists (H, c)\in \Psi,\ H\subseteq X$$
If there is an $$H, c$$ with $$H\subseteq X$$, then definitely the same $$H$$ will work if $$X$$ is taken to be larger!