伊莎貝爾：理解量詞的使用

Question

我發現我可以證明下面的引理，這對我來說似乎是錯誤的。

lemma assumes "∀a b. f a > f b ∧ a ≠ b" 
shows "∀a b. f b > f a" 
using assms by auto 

上述引理如何成立？ Isabelle是否像我使用過量詞一樣代替了數值？如果是這樣，我想說明a和b的所有值，f（a）大於f（b），我該如何做？

Answer 1

爲什麼它看起來不對？你是說任何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)？例如。對於任何一個和B，如果a ≠ b然後f a > f b？請注意，這仍然意味着f b > f a按照上面的例子，它實際上並沒有說任何有意義的東西。

Answer 2

你所說的引理是平凡的。幾乎是「A ==> A」的直接實例。從你的假設可以得出結論，∀a b. f a > f b。然後通過適當重命名綁定變量，我們獲得∀b a. f b > f a。此外，所有量詞可以重新排序以獲得∀a b. f b > f a。