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

[znmkhxrw (QQ)]

※ 引述《xcycl (XOO)》之銘言：
: 標題: Re: [其他] 等號需要定義 & 集合需要等號 嗎?
: 時間: Mon Nov 22 01:07:02 2021
:
: 先從有比較明確問題的回應
:
: 1. 如果考慮在沒有 = 的後設語言（或稱邏輯系統）
: 那在集合論中 = 的定義就是用 Axiom of Extensionality，
: 直覺來說就是具有一樣元素的視為一樣。一樣元素
: 這件事情不需要比對，單純用 implication => 就夠了。

不過看了wiki的ZF陳述與Axiom of Extensionality, "具有一樣的元素"這回事
其實是需要"屬於"的定義的

只是如同回覆原文a2大一樣, 在我往上追"屬於"的定義時, 查到這個結論:

集合公設裡面的"屬於"只是一個符號(雖然意義上代表元素裡面的成員)
而這個符號具有怎樣的性質, 就是其他公設所賦予的

:
: 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的那條公設本來就是這樣寫, 難道這公設有更廣的原型嗎?

:
: 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]到底算是長相不同嗎

而這些我覺得怪怪的地方在用集合論的函數定義就沒事了
所以我反而這樣才放心@@

順帶一題, 很常聽到"等號就是長相相同"這句話
嚴格說來我不喜歡也是因為何謂長相相同, 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) 不同數學基礎間都不相容?(即定義自己的系統和公理後)
(2) 有沒有可能A系統證明費馬最後定理是對的, 但是B證明是錯的?
    還是說整數系統如果相容於A系統, 那B系統就不可能有整數系統?
(3) 每種系統(可稱作集合論? ZF只是集合論的一種?)的接受度就是因人選擇
    無關對錯? 像是: (i) 如果(2)真的發生, 那也是看你選擇什麼系統
                    (ii) 我對於形式上的R[x]與等號覺得不舒服/不嚴謹
                         那也只是我的接受度問題, 等於我不太接受後設語言
                         覺得他不嚴謹罷了?

再次感謝回應~

--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 59.102.225.191 (臺灣)
※ 文章網址: https://www.ptt.cc/bbs/Math/M.1637525201.A.BD6.html
推 Vulpix      : [0]和[2]只是表示法，但本質是等價類。
推 Vulpix      : 所以「長相」要看定義，特別是表示法不唯一的時候
→ Vulpix      : 更不能漏掉定義。常見的例子除了Z/nZ以外，還有有
→ Vulpix      : 理數、有理式、有理數的連分數表示、有限小數也有
→ Vulpix      : 無窮小數表示等。
對阿! 舉我原文(E2)的例子:
嚴格說來 Z_2 := Z/~, where x,y€Z with x~y iff 2│x-y
其中: (Z  , =)中, "="是集合論的等號
      (Z_2, =)中, "="也是集合論的等號, 但是Z_2是那些收集等價類的集合

(E2)是問《(Z, @)合不合法, where @ 是Z上的新等號, say x@y iff x~y》
經過一些討論後
原本我也認同"既然都有(Z_2, =)這個嚴格的語言也不用定義新等號, 為何還要定義@"
也接受了"你要定義也可以, 只是要能化約成ZF集合論, 不然就是平行數學的基礎"

但是後來發現有理數Q, L^p空間, 我們其實都《相當於在寫(Z, @)》
因為嚴格說來:

(1) Q是等價類, 但是我們都直接寫 1/2 = 2/4, 但這個"="其實是"~"
(2) L^p是等價類, 但是我們都直接寫 |f|_p 而不是 |[f]|_p

最後就變成好像怎樣都可以...變成接受度的問題(?

→ recorriendo : 最後問題本來是問我的吧XD 那篇變太長了就懶得再加
→ recorriendo : 新東西
→ recorriendo : 簡單回：一般數學基礎的任務就是把數學編譯成不同
→ recorriendo : 的'低階語言' 在低階語言中找出目前數學所需的最必
→ recorriendo : 要規則 只有一部分人(同常是哲學家)才會嘗試去改動
→ recorriendo : 其中一些規則看看能不能得到不一樣的數學
→ recorriendo : 而不同的低階語言之間無從直接比較了(除非再把它們
→ recorriendo : 化約成更低階的語言) 重點是這不同的低階語言都確
→ recorriendo : 保了高階語言(數學)能有一樣的行為
→ recorriendo : 費馬最後定理 目前答案應該就是不知道 我們光知道
→ recorriendo : 它可以被數學證明 就夠難了 而知道一個結果動用到
→ recorriendo : 哪些前提 比起知道能得到這個結果又更難好幾倍 (不
→ recorriendo : 止數學 其他科目也一樣)
費馬的例子就是: 光用ZF集合論證明就曠日廢時了
                哪有心力去檢查其他集合論公設是否能證明
的意思嗎?

→ recorriendo : 數學基礎的歷史發展是看到數學家有很多理論 然後來
→ recorriendo : 找這些理論有沒有共同的基礎 不是反過來做  有些人
→ recorriendo : 像賺大錢沒事幹的Stephen Wolfram現在想反過來做
→ recorriendo : 不過那能做出什麼也不是大部分數學家關心的
讓我想到望月新一的論文很多人看不懂, 也是因為他用自己的語言跟基礎嗎@@?

→ xcycl       : 反過來找數學基礎的領域稱為 reverse mathematics
→ xcycl       : 也不是什麼賺大錢沒事幹的人做的吧
→ xcycl       : 化約的話不見得要翻成更低階的系統
→ recorriendo : 正統數學說的semantics是denotational semantics呀
→ recorriendo :  當然CS可以玩更多東西
→ recorriendo : 我所謂的反過來意思是窮舉一堆不相容的低階系統 看
→ recorriendo : 看各自能變出什麼數學
※ 編輯: znmkhxrw (61.231.64.215 臺灣), 11/22/2021 18:05:16
推 Vulpix      : 在不致引起混淆的情況下，都是省略[ ]的，畢竟多寫
→ Vulpix      : 就是麻煩。而且L^p其實用的不見得要是等價類，你可
→ Vulpix      : 以把不同函數視作不同，然後僅承認他們equal a.e.
→ Vulpix      : 。