理解謂詞邏輯中的一條棘手線條的困難

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]