| 中文题名： | 数学哲学中的构造主义 |
| 姓名： | |
| 保密级别： | 公开 |
| 论文语种： | 中文 |
| 学科代码： | 010101 |
| 学科专业： | |
| 学生类型： | 学士 |
| 学位： | 哲学学士 |
| 学位年度： | 2022 |
| 学校： | 北京师范大学 |
| 校区： | |
| 学院： | |
| 第一导师姓名： | |
| 第一导师单位： | |
| 提交日期： | 2022-06-11 |
| 答辩日期： | 2022-05-25 |
| 外文题名： | Constructivism in Philosophy of Mathematics |
| 中文关键词： | |
| 外文关键词： | |
| 中文摘要： |
在数学哲学中，构造主义断言有必要找到（或“构造”）一个数学对象的具体例子，以证明存在性命题的正确性。相比之下，在经典数学中，人们可以通过假设其不存在然后从该假设中推导出矛盾来证明数学对象的存在而无需明确地“找到”该对象。
﹀
构造主义有多种流派，其中包括由布劳威尔的直觉主义、马尔可夫的构造性递归数学、毕晓普的构造性分析，更现代的内容是构造主义类型论，如HoTT 和 Coq 等形式化证明助手。 本文首先总览构造主义的诸多流派，并选取代表人物的思想展开讨论，从语义学角度介绍直觉主义逻辑，阐述其对集合论和类型论的影响，最终对数学的未来提出展望。 |
| 外文摘要： |
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a concrete example of a mathematical object in order to prove the existential propositions. In classical mathematics, by contrast, one can prove the existence of a mathematical object without explicitly "finding" the object by assuming its non-existence and then deriving a contradiction from that assumption.
﹀
There are various schools of constructivism, including Intuitionism by Brouwer, Markov's constructive recursive mathematics, Bishop's constructive analysis, and the modern method is constructive type theory, such as formal proofs such as HoTT and Coq assistant. This paper firstly summarizes the many schools of constructivism, selects the representative ideas to discuss, introduce the semantics of intuitionistic logic, elaborate on its impact on set theory and type theory, and finally puts forward a prospect for the future of mathematics. |
| 参考文献总数： | 11 |
| 作者简介： | 无 |
| 插图总数： | 0 |
| 插表总数： | 0 |
| 馆藏号： | 本010101/22006 |
| 开放日期： | 2023-06-11 |
谷歌
