※ 引述《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://webptt.com/cn.aspx?n=bbs/Math/M.1637525201.A.BD6.html 对阿! 举我原文(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 最後就变成好像怎样都可以...变成接受度的问题(? 费马的例子就是: 光用ZF集合论证明就旷日废时了 哪有心力去检查其他集合论公设是否能证明 的意思吗? 让我想到望月新一的论文很多人看不懂, 也是因为他用自己的语言跟基础吗@@? ※ 编辑: znmkhxrw (61.231.64.215 台湾), 11/22/2021 18:05:16