(Co)-induction, fixpoints and inference systems

Question

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.

Answer 1

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!

You are correct about the identity deduction rules making co-induction trivial.