什么时候可以使用共归纳假设？

Question

当我们证明良序结构的属性时，我们可以使用归纳假设。我知道这是有证据的。

当谈到共归纳时，我很困惑。

另一个问题的答案之一“什么是共感应？”提到有一个核心递归定义的概念是格式良好的。

我（尝试）读到的许多与共归纳相关的东西大多谈论互模拟和等价。但据我所知，这些人试图证明两种共归纳数据结构的某种关系。例如，他们证明两个流是等价的。共归纳假设以某种方式源自互模拟假设之一。即便如此，我认为我仍然迷失于共归纳世界中构成良好性的要求。

我可以以某种方式看到，在证明这些命题时，共归纳假设是有效的，但我仍然不清楚它们何时可以用来证明更一般的命题，例如中提到的命题。 什么是共感应？. 。在该链接中，命题指出“某物是无限的”。这似乎是一种更通用的陈述形式，人们有兴趣证明。

一个可能相关的问题是任何命题是否可以转换并重述为等价命题。

是否有一些简单的非正式推理可以说明为什么共归纳适用于某些格式良好的要求？

我希望得到一个解释，如果可能的话： https://math.stackexchange.com/questions/432293/well-ordering-and-mathematical-induction/432302#432302.

Answer 1

首先，让我回忆一下最小和最大不动点 $\子集$. 。我们正在相对于某些集合进行工作 $U$, ，宇宙。在（共）归纳定义的情况下， $U$ 是所有项的集合。一个功能 $f:2^U o2^U$ （来自子集 $U$ 的子集 $U$） 是 单调, ， 如果 $A\子集B$ 总是暗示着 $f(A)\子集 f(B)$. 。A 固定点 的 $f$ 是一个集合 $A$ 这样 $f(A)=A$.

对于单调 $f$ 总有一个最小不动点 $\mu f$, ，即所有的交集 $A\subseteq U$ 这样 $f(A)\子集A$. 至少 意味着对于任意固定点 $F$ 我们总是有 $\mu f\subseteq F$.

举个例子，让 $f_{ t nat}$ 被定义为 $f_{ t nat}(A)=\{0\}\cup\{n+1\mid n\in A\}$. 。功能 $f_{ t nat}$ 是构造函数下的一步闭包函数 $0$ 和 $+1$. 。条件 $f_{ t nat}(A)\subseteq A$ 意思是 $A$ 在构造函数下关闭 $0$ 和 $+1$. 。交集意味着 $\mu f_{ t nat}$ 仅包含构造函数下每个封闭集合中的那些元素。这些恰好是自然数。该示例展示了自然数的归纳定义如何成为自然数构造函数下的最小闭包点。一般来说，归纳定义的集合是构造函数下闭包的最小不动点。

对偶，单调 $f$ 还有一个最大不动点 $ u f$, ，即所有的联合 $A\subseteq U$, ，使得 $f(A)\supseteq A$. 最伟大的 意味着对于任意固定点 $F$ 我们总是有 $ u f\supseteq F$. 。为了使对偶性完整，我们要注意交集是 $\子集$- 下确界和联合 $\子集$-supremum，因此 $\supseteq$-下确界。所以，事实上，最大不动点 $\子集$ 只是最小不动点 $\supseteq$ 反之亦然。（此外，请注意单调性要求对于 $\子集$ 至于 $\supseteq$.)

现在，介绍证明技术。让我们从自然数归纳法的例子开始。为了表明某些属性 $P$ 对于所有自然数都成立，我们证明 $P(0)$ 然后 $P(n)$ 暗示 $P(n+1)$. 。观看 $P$ 作为一个子集 $U$ （属性所包含的所有元素的集合），自然归纳法的证明义务是 $P$ 已关闭 $f_{ t nat}$. 。自然归纳法证明技术的正确性由最小不动点的定义得出：如果 $f_{ t nat}(P)\subseteq P$, ， 然后 $P$ 是形成交叉点的一部分 $\mu f_{ t nat}$, ，所以该属性自始至终都成立 $\mu f_{ t nat}$, ， 那是 $\mu f_{ t nat}\subseteq P$.

归纳法只是前一段对任意单调的概括 $f$ 代替 $f_{ t nat}$. 。共归纳是归纳的对偶：举证义务是 $f(P)\supseteq P$. 。这意味着如果 $P$ 保留某些元素 $x$, ， 然后 $x$ 仅使用基本元素构建 $P$ 也成立。因此，我们不是要证明该属性在构造函数的应用中仍然存在，而是必须证明它在解构中仍然存在。一旦满足举证义务，我们就得到 $ u f\supseteq P$.

结论有什么好处 $ u f\supseteq P$？让我们重新考虑一下 $P$ 不是作为财产，而是作为财产的子集 $U$. 。共归纳的结论表明，所有元素 $P$ 是共归纳定义集的良构成员 $ u f$。这就是示例中发生的情况 什么是共感应？ 显示 forall n, Infinite (from n). 。这里， $f$ 是构造函数下的闭包 Infinite （不属于 colist！） 和 $P$ 是该形式的所有项的集合 from n 对于一些 n.