你如何阅读 coq 量词`forall P: Set -> Prop`？答案

【问题标题】：How do you read the coq quantifier `forall P: Set -> Prop`?你如何阅读 coq 量词`forall P: Set -> Prop`？
【发布时间】：2019-11-20 23:13:07
【问题描述】：

我是 Coq 的新手，正在阅读 Mike Nahas 的教程：nahas_tutorial.v。具体来说，我无法理解下面给出的陈述：

Theorem forall_exists : (forall P : Set -> Prop,  (forall x, ~(P x)) -> ~(exists x, P x)).

这是我目前的解释，欢迎指正。

声明Set -> Prop 是一个可以扩展为forall s: Set, Prop 的命题，我将其理解为“对于Set 的每个证明（读取实例），我们也有Prop 的证明（实例） ”。

因此forall P : Set -> Prop 可以粗略地理解为“对于一个集合产生一个命题的每个证明”。

那么对于 (forall x, ~(P x))，我的猜测是 x 被 Coq 推断为 Set 类型，并且它被解读为“每个集合都会产生一个不可证明/错误的命题”。

对于~(exists x, P x)，我读到因为不存在暗示在 P 下存在真命题的集合。

这些看起来在逻辑上是等价的。我只是在语言上挣扎。 P 可以解释为从集合空间映射到命题空间的函数吗？我用过“产生”和“暗示存在”这样的短语；它是否正确？有没有更正确的说法？

感谢您的所有帮助！

编辑：对于任何有类似问题的人，我的困惑主要是对 Curry-Howard 同构的无知。

我的解释（可能仍然有点不稳定）现在该定理读作“对于每个谓词（布尔值函数）P 范围超过 Set 类型的元素，如果 P 下的每个集合的图像为假，则不存在P 产生True 的集合。”

【问题讨论】：

【解决方案1】：

Set -> Prop 属于Type，而不是Prop。当你在Type 时，X -> Y 应该读作从X 到Y 的函数，而当你在Prop 时，它应该读作X 意味着Y（尽管在库里-霍华德看来，这些都是一样的）。

当函数返回Prop 时，它通常被视为谓词或属性。所以forall P : Set -> Prop 可以读作“对于每个Set-valued 属性......”

【讨论】：

谢谢，这很有帮助。所以澄清一下，像forall a: b 这样的语句中冒号右侧的任何内容是否都在Type 中？该陈述中对冒号的解释是否与上面的白话行相同，所以我们读到定理forall_exists 的类型为(forall P : Set -> Prop, (forall x, ~(P x)) -> ~(exists x, P x))，即它是该陈述的证明？
是的，冒号右边的所有内容都在Type（或Prop 或Set）中，但它们是Type 的子类型。是的，声明 Theorem's、Definition's 和 Lemma's 本质上都是一样的：声明某种特定类型的术语。
我不同意：Set -> Prop 是函数的类型，其参数在 Set 中，其值在 Prop 中。所以它宁愿是Prop-valued，它已经通过说它是一个谓词来表达。我希望你说Set -> Prop 类型的对象P 是一个谓词，其范围涵盖Set 类型的元素，这是一种类型。这种谓词的一个例子是finite，表示给定类型是有限的，finite nat 不成立，而finite bool 成立，finite 的正确定义。