Re: [其他] 等號需要定義 & 集合需要等號嗎?

看板Math作者xcycl (XOO)時間2年前 (2021/11/22 13:40)推噓3(3推 0噓 8→)

留言11則, 1人參與討論串4/7 (看更多)

※ 引述《znmkhxrw (QQ)》之銘言： : ※ 引述《xcycl (XOO)》之銘言： : : 標題: Re: [其他] 等號需要定義 & 集合需要等號嗎? : : 時間: Mon Nov 22 01:07:02 2021 : : 先從有比較明確問題的回應 : : 1. 如果考慮在沒有 = 的後設語言（或稱邏輯系統） : : 那在集合論中 = 的定義就是用 Axiom of Extensionality， : : 直覺來說就是具有一樣元素的視為一樣。一樣元素 : : 這件事情不需要比對，單純用 implication => 就夠了。 : 不過看了wiki的ZF陳述與Axiom of Extensionality, "具有一樣的元素"這回事 : 其實是需要"屬於"的定義的 : 只是如同回覆原文a2大一樣, 在我往上追"屬於"的定義時, 查到這個結論: : 集合公設裡面的"屬於"只是一個符號(雖然意義上代表元素裡面的成員) : 而這個符號具有怎樣的性質, 就是其他公設所賦予的是的，集合論的公設主要描述 ∈ 這個 prediate 的性質跟操作。 : : 2. 在一階邏輯系統下，常見的定義是 Leibniz equality。 : : 直覺來說是 x = y 若對所有 predicate P 都有 P(x) 跟 P(y) 等價 : : （細究的話還要考慮邏輯系統怎麼建構設計的，要怎麼定義 P(x) 這類操作） : : 像是 reflexivity, symmetry 跟 transitivity 可以用這個定義導出來。 : : 系統上有了 = 之後，集合論上的 Axiom of Extensionality : : 敘述會修改成適合的形式，改成「對所有 x 在 A 為若且若 x 在 B」可推得 A = B。 : : 反過來從 Leibniz equality 可以得出。 : Wiki上寫的Leibniz equality確實就是定義成對所有 predicate P, P(x) <=> P(y) : 只是反射、對稱、遞移竟然可以由萊布尼茲的定義推出來我蠻訝異的XD : 也就是我原文的等號四公設其實可以保留第四個即可 : 另外你說"細究的話還要考慮邏輯系統怎麼建構設計的，要怎麼定義 P(x) 這類操作" : 這應該就是呼應我說的"即便自定義等號, 我不知道怎麼檢查第四公設" : 最後你說的"拓展公設可以改成「對所有 x 在 A 為若且若 x 在 B」可推得 A = B" : 我不太懂耶, wiki的那條公設本來就是這樣寫, 難道這公設有更廣的原型嗎? 這個版本的敘述用到了 = 但如果邏輯系統沒有 = 就得重新用集合論的語言定義等式，跟修改該條公設的敘述。StackExchange 有人討論過： https://math.stackexchange.com/questions/2718332/why-isnt-the-axiom-of-extensionality-considered-a-definition-of-equality 沒真的看過這樣的作法，雖然可以想像但就不予置評了。 : : 3. 後設語言上的「函數」跟集合論上的函數是不同層次的東西， : : 可以用純符號規則，定義出後設語言上函數的操作定義， : : 這一層獨立於集合論，沒有循環論證的問題。 : : （認為函數就是集合論定義的那套才是狹隘的觀點） : 原來集合論的函數定義是狹隘的... : 我一直以為集合論的函數定義才是嚴謹化的函數定義 : 像是函數的well-defined在一般的書是寫: for any a=b, f(a)=f(b) : 但是就覺得對每個a€A, f(a)就是你定義的一個值, 當然就那一個 : 之後遇到例子《f:Z_2→Z, f([x]) = x》, 才又知道well-defined這點是需要的 : 因為可能"a=b但是a,b長相不同", 不過以Z_2來說, [0]=[2]到底算是長相不同嗎 f([x]) = x 這樣的寫法有邏輯上的瑕疵。我們先定義了一個從 Z 到 Z 的函數 f'，然後檢查是否任意滿足 x ~ y 都會有同樣的結果 f'(x) = f'(y)，這時候我們才能說「存在一個 f 從 Z_2 -> Z 的函數」滿足 f'(x) = f([x]) = x （用沒必要的術語來說就是 coequaliser 的 universal property）這邊 [...] 的寫法可以視為 Z -> Z_2 的函數，把每個元素送到相對應的等價類上。長相不同這此例不適用。但邏輯系統本身會有一定程度的後設操作，像是邏輯述句上的變數代換這樣才有辦法談論 P(x) 中的 x 帶入某個 a 這種事情。在強一點後設語言下，甚至如 1 + 1 = 2 這種在集合論寫起來很囉唆的證明，會變成完全不需要在「系統內」證明，變成在後設語言內處理掉。 : 而這些我覺得怪怪的地方在用集合論的函數定義就沒事了 : 所以我反而這樣才放心@@ : 順帶一題, 很常聽到"等號就是長相相同"這句話 : 嚴格說來我不喜歡也是因為何謂長相相同, Z_2的[0]=[2], 左右長相一樣啊, : 都是一樣的Z的子集合, 只是代表符號不一樣 : 如此一來延伸一堆名詞: 長相, 代表符號...越來越奇怪 : 也正是因此, 我才會覺得純符號規則(後設語言?)會不嚴謹 : : 4. 聯集定義不涉及 = ，因為那是其中一項公理。 : : Axiom of Union 說給定一堆集合的集合 S ，存在一個集合 B 滿足 : : 對任意 S 裡頭的集合 A 以及任意 A 裡頭的元素 x 都會在 B 裡頭。 : 因為當初我沒用集合論, 直接反射想法是: : A∪B := {x│x€A or x€B} : x€A := 存在a€A 使得 a=x --(*) : 才會秒說涉及等號 : 不過之後發現我(*)對屬於的定義是錯的, 就沒事了 : : 5. Peano axiom 跟 ZF set theory 兩者沒有直接關係。 : : 後者可以用來建構前者的模型，用空集合代表 0, : : 然後 {0} 代表 1, {0, 1} 代表 2 依此類推下去。 : 我以為在ZF set theory上加入Peano axiom就能定義N, Z, Q... : 所以才認為Peano axiom是奠基在ZF : 意思是Peano axiom配合其他數學公設基礎也能定義N, Z, Q...了? 可以這樣說，或者說可以用「非」集合論的數學基礎上頭做數學論證。 : : 6. 一個數學物件不是集合（稱為 ur-element）在 ZF Set Theory : : 是不存在的，所有的符號都得編碼成某種集合去討論。 : : 有的集合論會允許這樣的物件存在。在其他的數學基礎如 Martin-Lof type theory : : 下則沒有這樣的困擾，只要滿足特定的形式就可以加。 : 了解! 知道ZF中每個都是集合, 所以我才會覺得原文r大說的"可化約成ZF集合論"很重要 : 多項式R[x]不管怎麼定義, 只要我接受ZF並且R[x]可以化約成ZF : 那對我來說是舒服且嚴謹的 : : 7. 最後等式的概念，也是目前數理邏輯跟理論電腦科學中研究非常活躍的題目， : : 何謂等式的證明跟等式如何計算等問題，到近幾年動用 homotopy theory : : 詮釋發展 homotopy type theory 跟以 cubical sets 數學概念 : : 發展的 cubical theory 是很多理論討論也充滿應用的領域，其中也有不少 : : 貢獻來自傳統的數學家，像是過世沒多久的費爾茲獎得主 Vladimir Voevodsky。 : : 才不是什麼走火入魔或是哲學才會問的問題 ... : 我會說走火入魔/哲學是因為像是這種: : (1) 為什麼1+1=2 : (2) 什麼是等號 : 這種問題問10個人應該有9個人會露出奇特的眼光吧XDDD : 我本身是會好奇這些問題的定義跟答案是什麼 : 但是親自go through一遍證明就沒啥興趣XD : : 後面回文的部分有點亂，就不一一回應了。（飄走） : 謝謝x大飄過來分享(~^O^~) : 除了以上回問的, 最後請教您三個問題: : (1) 不同數學基礎間都不相容?(即定義自己的系統和公理後) 數學基礎的討論早已不如從前。現在會討論公理系統可以用什麼數學結構詮釋，一來確保（相對）一致性，二來也是驗證公理的合理性像是集合論上很多 large cardinal 是其他集合論等價的擴充敘述得來的，用來比較不同公理的強弱性質。 : (2) 有沒有可能A系統證明費馬最後定理是對的, 但是B證明是錯的? : 還是說整數系統如果相容於A系統, 那B系統就不可能有整數系統? 我比較熟悉的是古典跟構造式數學的差異，而的確因為系統不同會有反古典的情況。也就是說在構造式數學中，有跟古典邏輯矛盾，卻跟構造式數學相容的描述，例如說「所有自然數上的 partial function 是可數的」但「自然數上的 total function 依然不可數」。但這並沒有什麼特別奇怪的，我們可以賦予這個基礎「計算函數」的詮釋，確保這些跟我們熟知的數學沒有衝突。數學基礎只是某種後設語言，平常數學論證是建構在這個語言之上，但需要的話我們可以把這語言的描述再翻譯（或說「化約」）到其他的數學結構上，目標數學結構上的結果。在這個手法下，後設語言中的「公理」並不是被視為不可質疑顯見的敘述，我們通常會找一個模型詮釋支持，而像是「排中律」這類也的確是可以用拓墣空間的詮釋來找到反例。用 CS 的術語應該很好理解，平常是用 A 語言（像是 JavaScript）寫程式，但編譯會經過各種中介語言最後是機械語言，數學大概可以理解成這種狀況。 : (3) 每種系統(可稱作集合論? ZF只是集合論的一種?)的接受度就是因人選擇 : 無關對錯? 像是: (i) 如果(2)真的發生, 那也是看你選擇什麼系統 : (ii) 我對於形式上的R[x]與等號覺得不舒服/不嚴謹 : 那也只是我的接受度問題, 等於我不太接受後設語言 : 覺得他不嚴謹罷了? 數學基礎或說後設語言的選擇的確無關對錯，看需求而已。而 ZF, ZFC 集合論數學基礎中是比較有名相對單純的，近代的 topos 的 internal logic 是用範疇論的框架談論分析各種集合論，同時說明相對應的數學詮釋應該具備什麼樣的性質。更近期的 homotopy type theory 不以集合的「屬於」為主體發展，改以「型別」的概念出發，賦予等式 = 的證明某種計算上的意義，在這基礎內的 Axiom of Univalance 可以導出「同構即可視作相同」的概念對於一般數學的討論可以避開集合論的麻煩（甚至代數結構間的同構概念是語言中自動掉出來的）。傳統的集合論也可以在此之上重新發展，也不限於構造式數學，可以將古典的排中律加入（雖然會破壞系統的計算性）。至於多項式表達的問題，大部分時候我們是用自然語言討論，只要符號的意義講清楚沒有歧異（例如對應到序列）可以接受就好。真的需要的話，是可以用另一套後設語言嚴格討論。 : 再次感謝回應~ -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 140.109.16.166 (臺灣) ※ 文章網址: https://www.ptt.cc/bbs/Math/M.1637559636.A.C42.html

推

Re: [其他] 等號需要定義 & 集合需要等號 嗎?

Re: [其他] 等號需要定義 & 集合需要等號嗎?