※ 引述《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://webptt.com/cn.aspx?n=bbs/Math/M.1637559636.A.C42.html 跟系统没有关系。 我这里指的是用 f([x]) = x 这种方式「定义函数」， 再来说明他是 well-defined 的意思其实一开始就不是在 quotient 上定义， 而是在没有做 quotient 之前的集合上定义，只是後续的检查告诉我们 对同一个等价类 [x] 得到的值都一样，这时候才可以说对该等价类上有了定义。 ※ 编辑: xcycl (140.109.16.166 台湾), 11/22/2021 20:00:59 ※ 编辑: xcycl (1.169.119.93 台湾), 11/22/2021 22:13:48 ※ 编辑: xcycl (1.169.119.93 台湾), 11/23/2021 00:37:12 ※ 编辑: xcycl (1.169.119.93 台湾), 11/23/2021 00:59:50