目录
28 关系: 同伦类型论，巴拿赫-塔斯基定理，二階邏輯，佩尔·马丁-洛夫，依赖类型，冯诺伊曼-博内斯-哥德尔集合论，全集，离散空间，策梅洛-弗兰克尔集合论，瓦茨瓦夫·谢尔宾斯基，证明论，鲁伊兹·布劳威尔，路德维希·维特根斯坦，阿尔弗雷德·塔斯基，艾伦·图灵，逻辑，恩斯特·策梅洛，格哈德·根岑，概念文字，朴素集合论，数学，数学危机，数学史，数学学科分类标准，数学哲学，数学领域，数理逻辑，替代公理。
同伦类型论
在数理逻辑与计算机科学中，同伦类型论（homotopy type theory，缩写 HoTT）是一套旨在于同伦论的大框架下构建内涵类型论语义的理论，尤指Quillen模型范畴和弱分解系统。反而言之，内涵类型论则为同伦理论提供了一套逻辑语言。类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论，因为集合论的语言难以转化成计算机证明辅助的形式语言。.
查看 数学基础和同伦类型论
巴拿赫-塔斯基定理
巴拿赫-塔斯基定理（或称豪斯多夫-巴拿赫-塔斯基定理，又名“分球怪论”），是一条数学定理。1924年斯特凡·巴拿赫和阿尔弗雷德·塔斯基首次提出这一定理。这一定理指出在选择公理成立的情况下，可以将一个三维实心球分成有限（不可测的）部分，然后仅仅通过旋转和平移到其他地方重新组合，就可以组成两个半径和原来相同的完整的球。巴拿赫和塔斯基提出这一定理原意是想拒绝选择公理，但该证明很自然，因此数学家认为这仅意味着选择公理可以导致少数令人惊讶和反直觉的结果。有些叙述中这条定理被看成是悖论，但是定理本身没有逻辑上不一致的地方，实际上不符合悖论的定义。.
二階邏輯
在逻辑和数学中，二阶逻辑是一阶逻辑的扩展，一阶逻辑是命题逻辑的扩展。二阶逻辑接着被高阶逻辑和类型论所扩展。 一阶逻辑和二阶逻辑都使用了论域（有时叫做“域”或“全集”）的想法。论域是可以在其上量化的个体元素的集合。一阶逻辑只包括取值为论域的个体元素的变量和量词。例如在一阶句子∀x(x ≠ x + 1)中变量x被用来表示一个任意的个体。二阶逻辑扩展了一阶逻辑，通过增加取值在个体的集合上变量和量词。例如，二阶句子\forall S \forall x \Big(x \in S \vee x \notin S \Big) 声称对于所有个体的集合S和所有的个体x，要么x在S中要么不在（这是二值原理）。最一般的二阶逻辑还包括量化在函数上的变量，和在下面语法章节解说的变量。.
查看 数学基础和二階邏輯
佩尔·马丁-洛夫
佩尔·埃里克·罗格·马丁-洛夫（Per Erik Rutger Martin-Löf，），瑞典逻辑学家、数理统计学家和哲学家。他以其在概率论基础方面的工作而闻名。自20世纪70年代以后，他的工作主要集中在逻辑学方面。在哲学逻辑方面，他的研究专注于蕴涵及判断学说，并在一定程度上受到了弗朗兹·布伦塔诺、弗雷格和胡塞尔先前工作的影响；在数理逻辑方面，他致力于创设直觉类型论作为数学的构造性基础。马丁-洛夫在类型论方面的工作深深地影响了计算机科学、尤其是后世编程语言理论的发展。 佩尔·马丁-洛夫是斯德哥尔摩大学的校友。直到2009年退休前，他一直担任斯德哥尔摩大学的数学和哲学学院的联合主席这一职务。, Academia Europaea, retrieved 2014-01-26.
依赖类型
在计算机科学和逻辑中，依赖类型（或依存类型，dependent type）是指依赖于值的类型，其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中，依赖类型可对应于谓词逻辑中的全称量词和存在量词；在依赖类型函数式编程语言如 ATS、Agda、Dependent ML、Epigram、F* 和 Idris 中，依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查，从而有效减少程序错误。 依赖类型的两个常见实例是依赖函数类型（又称依赖乘积类型、Π-类型）和依赖值对类型（又称依赖总和类型、Σ-类型）。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值，而非仅仅参数的类型，例如，一个输入参数为整型值n的函数可能返回一个长度为n的数组；一个依赖类型值对中的第二个值可以依赖于第一个值，例如，依赖类型可表示这样的类型：它由一对整数组成，其中的第二个数总是大于第一个数。 依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算，若允许在依赖类型中使用任意值的话，其类型检查将会成为不可判定问题；换言之，无法确保程序的类型检查一定会停机。 由于Curry-Howard同构揭示了程序语言的类型论与证明论的直觉逻辑之间的紧密关联性，以依赖类型系统为基础的编程语言大多同时也作为构造证明与可验证程序的辅助工具而存在，如 Coq 和 Agda（但并非所有证明辅助工具都以类型论为基础）；近年来，一些以通用和系统编程为目的的编程语言被设计出来，如 Idris。 一些以证明辅助为主要目的的编程语言采用强函数式编程（total functional programming），这消除了停机问题，同时也意味着通过它们自身的核心语言无法实现任意无限递归，不是图灵完全的，如 Coq 和 Agda；另外一些依赖类型编程语言则是图灵完全的，如 Idris、由 ML 衍生而来的 ATS 和 由 F# 衍生而来的 F*。.
查看 数学基础和依赖类型
冯诺伊曼-博内斯-哥德尔集合论
在数学基础中，冯·诺伊曼-博内斯-哥德尔集合论（von Neumann–Bernays–Gödel Set Theory，NBG）是设计生成同Zermelo-Fraenkel 集合论与选择公理一起（ZFC）同样结果的集合论公理系统，但只有有限数目的公理，即是不使用公理模式。 NBG首先由冯·诺伊曼在1920年代提出，從1937年开始由作修改，在1940年由哥德尔进一步简化。 不像ZFC，NBG只有有限多个公理。Richard Montague在1961年证明，不可能找到在逻辑上等价于ZFC的有限数目的公理；因此NBG的语言有能力谈论真类同谈论集合一样，并且关于集合的陈述在NBG中是可证明的，当且仅当它在ZFC中是可证明的（就是说NBG是ZFC的保守扩展）。.
全集
数学上，特别是在集合论和数学基础的应用中，全类（若是集合，则为全集）大约是这样一个类，它（在某种程度上）包含了所有的研究对象和集合。.
查看 数学基础和全集
离散空间
在拓扑学和相关数学领域中，离散空间是特别简单的一种拓扑空间，在其中点都在特定意义下是相互孤立的。.
查看 数学基础和离散空间
策梅洛-弗兰克尔集合论
梅洛-弗兰克尔集合论（Zermelo-Fraenkel Set Theory），含选择公理時常简写为ZFC，是在数学基础中最常用形式的公理化集合论，不含選擇公理的則簡寫為ZF。.
瓦茨瓦夫·谢尔宾斯基
茨瓦夫·弗朗西斯克·谢尔宾斯基（Wacław Franciszek Sierpiński），1882年3月14日生于华沙，1969年10月21日逝世于华沙。波兰数学家，以对集合论（对选择公理（axiom of choice）和连续统假设的研究）、数论、函数的理论和拓扑学的出色贡献而闻名。他共出版了超过700篇的论文和50部著作，这当中有两部，“一般拓扑学入门”（1934年）和“一般拓扑学”（1952年）后来被加拿大数学家Cecilia Krieger译成英文。 两个著名的分形是根据他的名字命名，谢尔宾斯基三角形和谢尔宾斯基地毯；另外还有谢尔宾斯基数和谢尔宾斯基问题也是以他的名字命名。.
证明论
证明论是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支，其主要兴趣在于证明论语义学的思想，该思想依赖于结构证明论的技术型想法才可行。.
查看 数学基础和证明论
鲁伊兹·布劳威尔
鲁伊兹·艾格博特斯·杨·布劳威尔(Luitzen Egbertus Jan Brouwer，多写作L.)(）是一位荷兰数学家和哲学家。他是数学直觉主义流派的创始人，也在拓扑学，集合论，测度论和复分析领域有很多贡献。.
路德维希·维特根斯坦
路德维希‧約瑟夫‧約翰‧维特根斯坦（Ludwig Josef Johann Wittgenstein，又譯维特根施泰因、維根斯坦；）是一名奧地利哲學家。他生于奥地利，后入英国籍。维特根斯坦是20世纪最有影响力的哲学家之一，其研究领域主要在语言哲学、心靈哲学和数学哲学等方面。1939年至1947年，任教於剑桥大学三一學院。Dennett, Daniel.
阿尔弗雷德·塔斯基
阿尔弗雷德·塔斯基（Alfred Tarski，），美国籍波兰裔犹太逻辑学家和数学家。塔斯基1939年移居美国，一直任教于加利福尼亚大学伯克利分校。华沙学派成员，广泛涉猎抽象代数、拓扑学、几何学、测度论、数理逻辑、集论和分析哲学等领域，专精于模型论、元数学、代数逻辑。 逻辑学家们将塔斯基的成就与亚里士多德、弗雷格、伯特兰·罗素和哥德尔相提并论。他的传记作者安妮塔和所罗门·费夫曼写道：“塔斯基和同时代的哥德尔一起改变了逻辑学在20世纪的面目，尤其是通过他对真值概念和模型论的研究。”Feferman, A.
艾伦·图灵
艾伦·麦席森·图灵，OBE，FRS（Alan Mathison Turing，又译阿兰·图灵，Turing也常翻譯成--林或者杜林，）是英国計算機科學家、数学家、邏輯學家、密码分析学家和理论生物学家，他被视为计算机科学與人工智慧之父。 在第二次世界大战期间，图灵曾在“政府密码学校”（GC&CS，今政府通信总部）工作。政府密码学校位于布萊切利園，是英国顶级机密情报机构。图灵在这里从事密码破译工作，有一段时间，他领导了（Hut 8）小组，负责德国海军密码分析。 期间他设计了一些加速破译德国密码的技术，包括改进波兰战前研制的机器，一种可以找到恩尼格玛密码机设置的机电机器。 图灵在破译截获的编码信息方面发挥了关键作用，使盟军能够在包括大西洋战役在内的许多重要交战中击败纳粹，并因此帮助赢得了战争。 图灵对于人工智能的发展有诸多贡献，例如图灵曾写过一篇名为《》的论文，提問「机器会思考吗？」（Can Machines Think?），作為一种用于判定机器是否具有智能的测试方法，即图灵测试。至今，每年都有试验的比赛。此外，图灵提出的著名的图灵机模型为现代计算机的逻辑工作方式奠定了基础。 图灵是著名的男同性恋者，并因为其性倾向而遭到当时的英国政府迫害，职业生涯尽毁。他亦患有花粉过敏症。 图灵还是一位世界级的长跑运动员。他的马拉松最好成绩是2小時46分03秒（手動計時），比1948年奥林匹克运动会金牌成绩慢11分钟。1948年的一次跨国赛跑比赛中，他跑赢了同年奥运会银牌得主。.
查看 数学基础和艾伦·图灵
逻辑
邏輯（λογική；Logik；logique；logic；意大利语、西班牙语、葡萄牙语: logica），又稱理則、論理、推理、推論，是对有效推論的哲學研究。邏輯被使用在大部份的智能活動中，但主要在哲學、心理、学习、推论统计学、脑科学、數學、語義學、 法律和電腦科學等領域內被視為一門學科。邏輯討論邏輯論證會呈現的一般形式，哪種形式是有效的，以及其中的謬論。 邏輯通常可分為三個部份：歸納推理、溯因推理和演繹推理。 在哲學裡，邏輯被應用在大多數的主要領域之中：形上學/宇宙論、本體論、知識論及倫理學。 在數學裡，邏輯是指形式逻辑和数理邏輯，形式逻辑是研究某個形式語言的有效推論。主要是演繹推理。 在辯證法中也會學習到邏輯。数理邏輯是研究抽象邏輯关系和数学基本的问题。 在心理、脑科学、語義學、 法律裡，是研究人类思想推理的处理。 在学习、推论统计学裡，是研究最大可能的结论。主要是歸納推理、溯因推理。 在電腦科學裡， 是研究各种方法的性质，可能性，和实现在机器上。主要是歸納推理、溯因推理，也有在歸納推理的研究。 从古文明开始（如古印度、中國和古希臘）都有對邏輯進行研究。在西方，亞里斯多德將邏輯建立成一門正式的學科，並在哲學中給予它一個基本的位置。.
查看 数学基础和逻辑
恩斯特·策梅洛
恩斯特·策梅洛（德语：Ernst Friedrich Ferdinand Zermelo，），生于柏林，是德国数学家，其工作主要為数学基础，因而对哲学有重要影响。.
查看 数学基础和恩斯特·策梅洛
格哈德·根岑
格哈德·根岑（Gerhard Karl Erich Gentzen，）是德国的数学家和逻辑学家。 他生于德国的格赖夫斯瓦尔德，在1929年到1933年期间是赫尔曼·外尔在哥廷根大学的学生之一。在1934年到1943年間他是大卫·希尔伯特在哥廷根大学的助手。從1943年起他是布拉格大學的教授。他的主要工作是数学基础中的证明论，特别是自然演绎和相继式演算。他的切消定理是证明论语义的基石，《逻辑演绎研究》中的某些哲学评论和维特根斯坦的格言"意义是使用"一起建立了推论角色语义的基础。 他是納粹黨和沖鋒隊的成員，在1945年5月7日隨所有在布拉格的德國人一起被逮捕之后，饿死于布拉格附近的战俘营中。.
查看 数学基础和格哈德·根岑
概念文字
《概念文字》是1879年出版的戈特洛布·弗雷格写的一本关于逻辑学的书。书名《Begriffsschrift》通常翻译成《Concept Writing》或《Concept Notation》；书的完整标题把它标识为《模仿算术的纯思维的形式语言》。这本小书无可争议是亚里士多德之后在逻辑学领域最重要的出版物。弗雷格开发他的形式逻辑系统的动机是类似于莱布尼兹对“演算推论器”的渴望。 弗雷格定义了逻辑演算来支持他在数学基础上的研究。“概念文字”是书和其中定义的演算二者的名字。.
查看 数学基础和概念文字
朴素集合论
在纯数学中，朴素集合论是是探討数学基础時，用到的幾個集合論中的一個，朴素集合论主要是將用一般語言的形式處理集合問題，依赖於把集合作为叫做这个集合的“元素”或 “成员”的搜集（collection），未有形式化的理解。和用公理定義而產生的公理化集合论不同。 而公理化集合论只使用明确定义的公理列表，還有從中证明的关于集合和成员关系的種種事实，公理起源自对对象的搜集和它们的成员的理解，但为了各种目的而被謹慎地构建，例如是避免已知的各種悖论，例如理发师悖论－一個理髮師他只為（而且一定要為）城裡所有不為自己刮鬍子的人刮鬍子，那理髮師該為自己刮鬍子嗎？ 集合在数学中是极其重要的；事實上，採用现代的形式化定義，多種数学对象（数、关系、函数等等）都可以用集合来構建。.
查看 数学基础和朴素集合论
数学
数学是利用符号语言研究數量、结构、变化以及空间等概念的一門学科，从某种角度看屬於形式科學的一種。數學透過抽象化和邏輯推理的使用，由計數、計算、量度和對物體形狀及運動的觀察而產生。數學家們拓展這些概念，為了公式化新的猜想以及從選定的公理及定義中建立起嚴謹推導出的定理。 基礎數學的知識與運用總是個人與團體生活中不可或缺的一環。對數學基本概念的完善，早在古埃及、美索不達米亞及古印度內的古代數學文本便可觀見，而在古希臘那裡有更為嚴謹的處理。從那時開始，數學的發展便持續不斷地小幅進展，至16世紀的文藝復興時期，因为新的科學發現和數學革新兩者的交互，致使數學的加速发展，直至今日。数学并成为許多國家及地區的教育範疇中的一部分。 今日，數學使用在不同的領域中，包括科學、工程、醫學和經濟學等。數學對這些領域的應用通常被稱為應用數學，有時亦會激起新的數學發現，並導致全新學科的發展，例如物理学的实质性发展中建立的某些理论激发数学家对于某些问题的不同角度的思考。數學家也研究純數學，就是數學本身的实质性內容，而不以任何實際應用為目標。雖然許多研究以純數學開始，但其过程中也發現許多應用之处。.
查看 数学基础和数学
数学危机
數學危機在歷史上發生過三次，每一次均對數學的發展有重大影響。在第一次數學危機中，因為發現腰長為1的等腰直角三角形的斜邊長度無法寫成有理數，從而引申出日後的無理數概念。第二次數學危機得解決微積分引入無窮小量而產生的問題。第三次數學危機則是因羅素悖論而起，它點出樸素集合論中的缺失。 Ernst Snapper所著The Three Crises in Mathematics: Logicism, Intuitionism, and Formalism, Mathematics Magazine, Vol.
查看 数学基础和数学危机
数学史
数学史的主要研究对象是历史上的数学发现，以及调查它们的起源，或更广义地说，数学史就是对过去的数学方法与数学符号的探究。 数学起源于人类早期的生产活动，为古中国六艺之一，亦被古希腊学者视为哲学之起点。數學最早用於人們計數、天文、度量甚至是貿易的需要。這些需要可以簡單地被概括為數學對結構、空間以及時間的研究；對結構的研究是從數字開始的，首先是從我們稱之為初等代數的——自然數和整數以及它們的算術關係式開始的。更深層次的研究是數論；對空間的研究則是從幾何學開始的，首先是歐幾里得幾何和類似於三維空間（也適用於多或少維）的三角學。後來產生了非歐幾里得幾何，在相對論中扮演著重要角色。 在进入知识可以向全世界传播的现代社会以前，有记录的新数学发现仅仅在很少几个地区重见天日。目前最古老的数学文本是《普林顿 322》（古巴比伦，约公元前1900年），《莱因德数学纸草书》（古埃及，约公元前2000年-1800年），以及《莫斯科数学纸草书》（古埃及，约公元前1890年）。以上这些文本都涉及到了如今被称为毕达哥拉斯定理的概念，后者可能是继简单算术和几何后，最古老和最广泛传播的数学发现。 在公元前6世纪后，毕达哥拉斯将数学作为一门实证的学科进行研究，他创造了古希腊语单词μάθημα（mathema），意为“（被人们学习的）知识学问”。希腊数学家在相当大的程度上改进了这些数学方法（特别引入了演绎推理和严谨的数学证明），并扩大了数学的主题。中国数学做了早期贡献，包括引入了位值制系统。如今大行于世的印度-阿拉伯数字系统和运算方法，很可能是在公元后1000年的印度逐渐演化，并被伊斯兰数学家通过花拉子米的著作将其传到了西方。伊斯兰数学则将以上这些文明的数学做了进一步的发展贡献。许多古希腊和伊斯兰数学著作随后被翻译成了拉丁文，引领了中世纪欧洲更深入的数学发展。 从16世纪文艺复兴时期的意大利开始，算术、初等代数及三角学等初等数学已大体完备。17世纪变数概念的产生使人们开始研究变化中的量与量的互相关系和图形间的互相变换。随着自然科学和技术的进一步发展，为研究数学基础而产生的集合论和数理逻辑等也开始慢慢发展。 从古代到中世纪，数学发展的历史时期都伴随着数个世纪的停滞，但从16世纪以来，新的数学发展伴随新的科学发展，让数学不断加速大步前进，直至今日。.
查看 数学基础和数学史
数学学科分类标准
数学学科分类标准(MSC) 是由美国数学学会策划的建立在两个主要的引文数据库数学评论和数学文摘的字母数字混合的分类方案.
数学哲学
数学哲学是哲学的一个分支，研究数学中的哲学问题的学科。从毕达哥拉斯到康德的众多思想家都有许多数学哲学的重要思想，但作为专门学科直到19世纪中叶以后才逐渐建立起来。着重研究：.
查看 数学基础和数学哲学
数学领域
随着数学史的推移，数学已成为一个极广泛的主题，因此有必要对不同的数学领域进行分类。许多不同的分类方案已经出现，有相同点也有不同点，差异的原因主要是它们使用的目的不同。此外，随着数学的发展，这些分类方案也必须随之发展，以解释新创建的领域或者新发现的不同领域间的联系。分类通常是困难的，对于那些最活跃的，跨越不同领域边界的主题往往更加困难。 数学的传统分支被分类到纯数学，主要研究其内在的逻辑性；而应用数学可以直接应用以解决现实问题。 这种分类方法并不十分清晰，许多主题是按照纯数学发展的，但后来就发现了意想不到的应用。宽泛的分类方法，例如离散数学和计算数学，就是最近才出现的。.
查看 数学基础和数学领域
数理逻辑
数理逻辑是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。 数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学，后者的使用现已局限于证明论的某些方面。.
查看 数学基础和数理逻辑
替代公理
在公理化集合论和使用它的逻辑、数学和计算机科学分支中，替代公理模式是 Zermelo-Fraenkel 集合论的一个公理模式，它本质上断言一个集合在一个映射（泛函谓词）下的像也是一个集合。它对于构造特定的大集合是必需的。.
查看 数学基础和替代公理