Я обнаружил, что могу доказать следующую лемму, которая кажется мне ложной.Изабель: понимание использования кванторов
lemma assumes "∀a b. f a > f b ∧ a ≠ b"
shows "∀a b. f b > f a"
using assms by auto
Как можно утверждать, что приведенная выше лемма верна? Является ли Изабель заменой значений, поскольку я использовал квантор ifier? Если это так, я хочу указать для всех значений a и b, f (a) больше f (b), как бы я это сделал?
Почему это кажется ложным? Вы заявляете, что для ЛЮБОГО a и b, f a > f b и a ≠ b. Это означает, что если говорят a = 0 и b = 1, то f 0 > f 1, но и когда a = 1 и b = 0 это означает, что f 1 > f 0.
Кроме того, вы принимаете ∀a b. f a > f b ∧ a ≠ b, это означает, что вы ДОЛЖНЫ ПРИНИМАТЬ, что для любых a и b, f a > f b И отличается от b. Это, как правило, неверно, поскольку у вас не может быть ∀a b. a ≠ b
Возможно, вы хотели сказать следующее: ∀a b. (a ≠ b ==> f a > f b)? например. для любых a и b, если a ≠ b, то f a > f b? Обратите внимание, что это все еще подразумевает f b > f a, как в примере выше, это действительно не говорит ничего значимого.
Лемма, которую вы заявляете, тривиально верна. Почти прямой экземпляр «A ==> A». Из вашего предположения можно тривиально сделать вывод, что ∀a b. f a > f b. Затем, переименовав связанные переменные, получим ∀b a. f b > f a. Более того, все кванторы могут быть переупорядочены для получения ∀a b. f b > f a.
Я понимаю, я был в замешательстве. Как я представляю для a в множестве S, f a больше f b, где b также принадлежит множеству S? – creator22
Вместо '∀a b. a ≠ b ==> f a> f b' (который анализируется как '(∀a b. a ≠ b) ==> f a> f b'), вы, вероятно, хотите' ∀a b. a ≠ b -> f a> f b'. –
Обратите внимание, что это, вероятно, не то, что вы хотите, потому что это будет означать, что для любых 'a' и' b' с 'a ≠ b' у вас есть как' f a f b'. Это не должно зависеть от разумного заказа. –