Re: [其他] "等於"的定義 反對稱性

[xcycl (XOO)]

※ 引述《ppu12372 (高能兒)》之銘言：
: https://zh.m.wikipedia.org/zh-tw/%E7%AD%89%E4%BA%8E
: 維基百科的定義是:
: 集合A上一種滿足自反性，對稱性，反對稱性和傳遞性的二元關係
: 自反性、對稱性、和傳遞性就是等價關係嘛，所以照他所述，等於和等價就差在反對稱
性
: 但我點進去反對稱性的說明後發現
: "若對所有的M搣轏，若鰜Y到bB鰜Y到a，則 a = b"
: 如果拿它來定義等於，他的敘述中包含了等號，就循環定義了
: 再往下看("等於"的條目)
: 下面有提到替代性
: 用滿足替代性的等價關係來定義等於好像沒問題，但我後來有查到有個條目叫等量公理
，
: 問題是，非邏輯公理不就是公設嗎？
: 代表我們可以建構另一個不滿足等量公理卻用到"等於"這個概念的公理系統
: 就像歐幾里德幾何第五公設可以換掉一樣
: 所以"等於"到底該怎麼定義？
: -----
: Sent from JPTT on my Asus ASUS_Z00AD.
英文 Wikipedia 上有不少內容，不過稍微爬梳也幫我自己複習一下。

在二階邏輯下，也就是量詞 for all ... 跟 for some ... 可以不單指元素，
 還可以指集合的情況下， x = y 可以定義成

For all P, P x if and only if P y

白話說 x 等於 y 代表對任意的性質，如果 x 滿足則 y 也滿足，反之亦然，

稱為萊布尼茲等式（Leibniz's equality）。從這個定義出發，
我們可以證明等號 = 是一個等價關係，以及替代性等性質。因為定義用到
了對所有的「性質」，在一階邏輯下沒辦法定義得用到二階。

除此之外，如果系統內已經有一個等式是用公設定義出來的等式
我們還可以證明兩者種等式是等價。

以上情況是單看在二階邏輯的情況，加入集合論後，
要說集合相等，加入外延公設 Axiom of Extensionality
也就是說「若 X, Y 有一樣的元素，則 X = Y」。反過來
則是用 Leibniz 等式的定義推得。

接下來拿掉 Extensionality 也是可以找到滿足的模型，底下

http://math.stackexchange.com/questions/63910/example-of-a-model-in-set-theory
-where-the-axiom-of-extensionality-does-not-hold

有舉一個簡單的例子。但事情其實還沒結束，Wikipedia 跟 MathOverflow
有不少線索指引，包括像是把一般的集合論塞到沒有等式的集合論，
或是分類等式的意義，Leibniz's equality 變成可以證明之類的...

大概就這樣吧。


--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 76.93.217.199
※ 文章網址: https://www.ptt.cc/bbs/Math/M.1472632404.A.660.html
推 alfadick    : 所以起初集合論的"相等" 並不等於二階邏輯的"相等"
→ alfadick    : 嗎? 是後來下一步才能證明出來,集合論的相等等價那
→ alfadick    : 個二階邏輯定義的相等
→ xcycl       : 集合論的等式是二階邏輯的等式，只是多加一個條件要
→ xcycl       : 求集合內容一樣的話，兩個集合也要一樣。如果系統沒
→ xcycl       : 有等式也可以另外作一個出來就是
→ xcycl       : 但或許可以強調一點：集合論是建立在邏輯系統之上的
→ xcycl       : Leibniz 等式也只不過是二階邏輯下的一種定義
→ xcycl       : 在其他的邏輯系統下可能會有不同的等式定義
→ xcycl       : 要捕捉的哲學意涵也不盡相同。
→ recorriendo : 「等於」一般都視作初基 也就是無定義
→ recorriendo : 證明系統中就是把它視為一個可以引用相關公設的特殊
→ recorriendo : 符號而已
→ recorriendo : 而至於在模型論理要規範等於的意義 則又要訴諸meta-
→ recorriendo : language裡的等於 所以...沒完沒了XD
推 suhorng     : 回歸 MLTT, 訴諸 judgemental equality 耶耶耶