合金中的高阶量化

Question

我在阅读有关合金中更高阶的量化，并看到以下内容：孤独p：一些X | F
现在，如果关键字'some'修饰p或X，我感到困惑。这是否意味着X应该是非空的或者是否意味着p的基数应该大于1。

Answer 1

在这种情况下，“some”修改“X”，这意味着X应该是非空的。但是，“孤独”仍然会修改“p”，这意味着基数p < = 1.换句话说，这个约束表明非空集合“X”中至多有一个“p”，使得“F”成立。