如何读取coq量词` `forall : Set -> Prop`？

Question

我是一个全新的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，如果P下的每个集合的图像都是假的，那么就没有P生成True的集合。”

Answer 1

Set -> Prop属于Type，不属于Prop。当你在Type中时，X -> Y应该作为一个函数从X读到Y，当你在Prop中时，它应该被读作X暗示的Y (尽管库里-霍华德认为这是相同的)。

当一个函数返回一个Prop时，它通常被认为是一个谓词或属性。因此，可以将forall P : Set -> Prop读作"for every Set-valued property...“