理解谓词逻辑中的一条棘手线条的困难

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彼此不相等，但考虑到这个公式的长度，答案感觉有点迟钝。

任何帮助将是巨大的，THX，有一个愉快的一天

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] 

但是这一次不（反例：我挑我= 1，J = 3，K = 2）：

[1;2;3]