难以理解谓词逻辑中的棘手行

Question

我很难解释这个来自我正在经历的过去试卷的公式。 xs 是自然数列表 ([Nat])，i、j、k 是 Nat 排序的。 in(n,xs)函数表示自然数n存在于列表xs中。

∀i∀j∀k(in(i,xs) ^ in(j,xs) ^ in(k,xs) -> i=j v j=k v i=k)

我想我理解所有个别含义：

∀i∀j∀k                                    ; for all Nats i, j, k
in(i,xs) ^ in(j,xs) ^ in(k,xs)             ; are in list xs
i=j v j=k v i=k                            ; at least 2 of i, j, k have the same number

但我不能走得更远。我首先认为这是说每个数字都带有相同的值，因为它并不表示 i、j 和 k 彼此不相等，但考虑到答案感觉有点迟钝这个公式的长度。

任何帮助都会很棒，谢谢，祝你有美好的一天

Answer 1

你的公式说：

∀i∀j∀k                                    ; take three arbitrary Nat-s
in(i,xs) ^ in(j,xs) ^ in(k,xs)             ; if all three are in the sme list xs
->                                         ; then
i=j v j=k v i=k                            ; at least 2 of them are equal

因此your list does not contain three distinct numbers。它可能包含任意数量的 Nats。它可以包含任意数量的单个 Nat 副本。它也可以是空的。

这是一个验证您的财产的清单：

[1;1;1;1;2;2;2;2;2;1;1;1;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2;2]

如果您重复它任意次数（将其连接到自身），可能无限次，它仍然会验证您的属性。这也验证了您的属性：

[1;2]

但这个没有（反例：我选择 i=1,j=3,k=2）：

[1;2;3]