我是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下的“ false”，则没有P产生True的集合。”