проблемы с пониманием сложной линии в логике предикатов

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

Следовательно ваш список не содержит трех различных чисел . Может содержать произвольное количество Натс. Он может содержать произвольное количество копий одного 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]