集合推导与量词 ∀ ∃

选一个谓词 P：满足它的元素在全集里高亮，{x ∈ U | P(x)} 即时列出；下方两枚徽章判定 $\exists$ 与 $\forall$ 是否成立，并给出见证（一个满足的元素）或反例（一个不满足的元素）。

两条常被用到的规则：量词与否定对偶——$\neg \exists x P(x)$ 等价于 $\forall x \neg P(x)$（「没有一个满足」=「所有都不满足」），$\neg \forall x P(x)$ 等价于 $\exists x \neg P(x)$（「并非都满足」=「存在一个不满足」）。另外，空集上的 $\forall$ 恒真（vacuous truth，「所有」没有对象可反驳），而空集上的 $\exists$ 恒假。

写进代码：集合推导 {x ∈ U | P(x)} 就是 U.filter(P)；量词 $\exists$ / $\forall$ 对应 some / every——它们对空数组的取值（[].some() 为假、[].every() 为真）恰好是 vacuous truth 的落地。