0
$\begingroup$

I'm rather stuck with the example of proof by coinduction, as generally known the principle is written as:

$$ P\subseteq F(P)\implies P\subseteq \nu F $$

in an old problem When can the coinduction hypothesis be used, the answer said that we should treat $P$ as a subset of $U$, and the principle of coinduction guarantees that if $P\subseteq F(P)$, then $P\subseteq \nu F$ can be interpreted as "all elements of $P$ are some well-formed elements of $\nu F$", which I don't particularly understand, what is the relation between $P$ and $\nu F$, further, take as example the subtyping relation over infinite types, we would define $F$ to be

$$ F(S) = \lbrace (\bot, \top) \rbrace \cup \lbrace (S1\times S2), (T_1\times T_2) \ |\ (S_1, T_1), (S_2, T_2)\in S\rbrace \cup\lbrace (S1\rightarrow S2), (T_1\rightarrow T_2) \ |\ (T_1, S_1), (S_2, T_2)\in S\rbrace $$

now clearly $\nu F$ will be the set of infinite subtyping relations (not finite subtyping relation over infinite types), then what would $P$ be? what's the relationship between it and $\nu F$?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ $P$ is universally quantified; it can be any subset of $U$. $\endgroup$ Commented Oct 14, 2024 at 16:29
  • $\begingroup$ @NaïmFavier So you mean that the $U$ itself can be $P$ and thus justifying all elements of $U$ also satisfy the condition $\endgroup$ Commented Nov 15, 2024 at 3:23

0

Reset to default

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.