1
$\begingroup$

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.

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

1 Answer 1

0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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