数学2018home.sandiego.edu
构造数学的奇妙世界（2017）
The weird and wonderful world of constructive mathematics (2017)
入门 · 约 45 分钟读完前置知识：数学证明基础、一阶逻辑基础
导读
这篇论文（Shulman《构造性数学的奇异而精彩的世界》）通俗地介绍了构造性数学：一种不依赖排中律等非构造性原则的数学体系，其中存在性证明必须给出具体构造。文章解释了构造性数学与经典数学的差异，例如在构造性框架下可能存在 d²=0 但无法证明 d=0 的数，并说明许多经典定理在构造性视角下仍有对应版本。
HN 关注点：HN 读者对构造数学与直觉主义逻辑、可计算性与经典数学的关系这一话题长期感兴趣，讨论焦点集中在排中律的取舍及构造性证明的实际含义。
HN 评论精选
这几条评论里：质疑 1 补充 3
补充补充推荐 Bauer 的相关演讲视频与论文作为延伸资料
这里很多人想了解更多，推荐 Andrej Bauer 的同一主题演讲，有视频和论文两个版本，内容基本相同。
jimhefferon查看英文原文
There are a lot of folks here asking for a bit more. Here are two versions of the same well-done talk, from Andrej Bauer: a video https://www.youtube.com/watch?v=21qPOReu4FI, and a paper http://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/ (sorry, the paper link may not work for everyone, but the video contains basically the same content.)
补充从逻辑角度解释构造性数学与直觉主义逻辑的关系及存在量词的推理规则
排中律只是经典数学非构造性的一个方面，去掉它得到直觉主义逻辑；每个直觉主义定理都蕴含经典定理，反之经典定理也等价于某个直觉主义定理。另一个非构造性方面是结论含存在量词的公理，作者随后用推理规则示例说明存在量词的使用方式。
vladsotirov查看英文原文
The remarks on computable and continuous functions can also be thought about as follows. The law of the excluded middle is only one non-constructive aspect of classical mathematics. Dropping it leaves you with what is usually called "intuionistic logic", and the characterization of constructive mathematics as broader than classic mathematics is literally correct in that every intuionistic theorem implies a classical theorem, and every classical theorem is equivalent to an intuionistic theorem. Another non-constructive aspect of classical mathematics, which remains non-constructive in intuionistic logic, are axioms whose conclusion involves the existential quantifier. In both classical and intuionistic logic, the inference rule, which governs how the existential quantifer may be used, looks as follows. > Asserting that "the existence of x such that phi(x) holds entails psi" where x is a variable bound by the existential quantifer and not occurring in psi, is equivalent to assering that "phi(y) entails psi" where y is a free variable not ocurring in psi. This inference rule (assembly language of logic) seems weird, so an example of its use might help. > "there exists x such that phi(x) holds entails that there exists x such that phi(x) holds" by tautological inference, and by the existential quantifier inference we have that "phi(y) entails the existence of x such that phi(x) holds" where y is a free variable not appearing in "exists x such that phi(x) holds". When doing classical or intuionistic mathematics, you would usually use axioms of the form "psi entails that there exists x such that phi(x) holds". But such axioms are non-constructive because the inference rule does not allow you to start with "there exists x such that phi(x) holds" and somehow construct an actual term t such that phi(t) holds. Now what Mike says in his slides is that it is consistent to modify intuionistic mathematics into a "fully constructive mathematics" by strengthening the existential quantifier so that "exists x such that phi(x) holds" would imply that we can (computably) come up with a specific term t such that phi(t) holds. As a consequence, any statement in fully constructive mathematics involving the existential quantifier as a conclusion is a stronger statement than such in classical mathematics, which is roughly why all functions end up being continuous: the definition of the notion of a function itself requires that the function be computable, i.e. that its values exist in the sense of the strengthened existential quantifier.
质疑质疑论文中 d²=0 例子与直觉主义初衷的相容性
论文说构造数学中可以有 d²=0 但不一定 d=0 的数，脚注说 d 不是实数。我觉得很困惑——这似乎是用一个刻意不可构造的数来辅助构造数学的证明？这与直觉主义数学的目标（摒弃选择公理式证明荒谬结论如 Banach-Tarski）似乎直接相悖。
andrewla查看英文原文
> In constructive mathematics, there can also be numbers d such that d^2 = 0 but not necessarily d = 0. In the footnote, it mentions that d is not a real number (which seems right). But I find this very confusing -- this seems to be using a deliberately non-constructible number to facilitate proofs in constructive mathematics? Regardless of whether this meets a formal criteria for being a tool in constructive mathematics, it does seem to be in direct opposition to the notion of intuitionalist mathematics, which has as a fundamental goal to dispense with axiom-of-choice-style proofs of things that are clearly ridiculous (like Banach-Tarski).
补充询问论文幻灯片/排版所用的工具
总看到数学里用这种幻灯片模板，大家是用什么做的？是特定的 PowerPoint 模板吗？
laichzeit0查看英文原文
Always see this type of slide template used in mathematics. What do people use to build these slides? Is it a specific powerpoint template?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2018Hacker News 讨论帖166 分 · 68 评
同领域还值得读
一种新的相关系数
A New Coefficient of Correlation
提出了一种新的相关性系数（由 Sourav Chatterjee 提出），能够检测变量之间任意形式（不限于线性）的相关关系，且计算简单高效，主要基于排序和距离计算。
数学2021 · 682 分 · 158 评 · 引用 1进阶 · 约 60 分钟编辑精选数学的两种文化
The Two Cultures of Mathematics (2000)
这是数学家 Timothy Gowers 于 2000 年发表的一篇随笔，他把数学研究大致分成两种文化：一类是“解题者”，热衷于攻克具体难题、发展技巧（如组合数学）；另一类是“理…
数学2009 · 307 分 · 102 评入门 · 约 35 分钟编辑精选重新定义统计显著性
Redefine statistical significance
提议将统计显著性阈值从常用的 p<0.05 收紧到 p<0.005，以降低假阳性率、缓解可重复性危机。
数学2017 · 303 分 · 114 评入门 · 约 45 分钟编辑精选统计建模：两种文化（2001）
Statistical Modeling: The Two Cultures (2001)
讨论统计学中两种建模文化：一种假设数据由某种随机模型生成，侧重推断与系数解释；另一种把数据生成机制视为未知，侧重预测精度，主张使用算法建模。
数学2015 · 254 分 · 36 评进阶 · 约 60 分钟编辑精选通信的数学理论 (1948)
A Mathematical Theory of Communication (1948)
这是香农 1948 年的经典论文《通信的数学理论》，奠定了信息论的基础。
数学2016 · 169 分 · 53 评入门 · 约 90 分钟编辑精选