比浏览器更快的访问！
51 关系: Agda，原始递归函数，可判定性，多元组，外延，存在量化，实数，安德雷·柯爾莫哥洛夫，不交并，交換律，依赖类型，命题，命题逻辑，哲学家，内涵，函数空间，函數程式語言，全称量化，BHK释义，Coq，笛卡儿积，等价类，简单类型λ演算，类型论，类型检查，系统F，编程语言，真值，瑞典，直觉主义，直觉主义逻辑，非直谓性，谓词逻辑，鲁伊兹·布劳威尔，自然数，蕴涵，良基关系，集合论，逻辑，逻辑与，逻辑非，逻辑运算符，逻辑或，LEGO，Per Martin-Löf，柯里-霍华德同构，构造演算，有类型λ演算，数学家，数学归纳法，...，数学构造主义。 扩展索引 (1 更多) »
Agda
Agda是一个依赖类型的函数式编程语言，同时亦可作为一个用于构建构造性证明的证明辅助工具。Agda最早由瑞典查尔摩斯工学院的 Ulf Norell 设计并开发，作为他的博士论文课题。目前的版本，Agda 2，则在第一版的基础上完全重写。 Agda体现了柯里-霍华德同构（Curry-Howard correspondence）。它的理论根基是 Zhaohui Luo 的UTT，该理论与 Per Martin-Löf 的直觉类型论相类似。 Agda与Coq的几点显著不同之处在于：它本身并不支持tactics；所有的证明均以函数式编程的方式书写；语言本身吸收了许多常规的程序语言元素，诸如：数据类型、模式匹配（pattern matching）、记录类型（records）、let表达式和模块（modules）等，而其语法则非常类似Haskell。 Agda系统一般通过其提供的Emacs界面进行交互，亦可藉由命令行方式单独执行。.
新！!: 直觉类型论和Agda · 查看更多 »
原始递归函数
在可计算性理论中，原始递归函数（primitive recursive functions）对计算的完全的形式化而言是形成重要构造板块的一类函数。它们使用递归和复合作为中心运算来定义，并且是递归函数的严格的子集，它们完全是可计算函数。通过补充允许偏函数和介入无界查找运算可以定义出递归函数的更广泛的类。 通常在数论中研究的很多函数，近似于实数值函数，比如加法、除法、阶乘、指数，找到第 n 个素数等等是原始递归的（Brainerd and Landweber, 1974）。实际上，很难设计不是原始递归的函数，尽管某些函数是已知的(比如阿克曼函数)。所以，通过研究它们，我们能发现有广泛影响的结论的那些性质。 原始递归函数可以用总是停机的图灵机计算，而递归函数需要图灵完全系统。 原始递归函数的集合在计算复杂性理论中叫做PR。.
新！!: 直觉类型论和原始递归函数 · 查看更多 »
可判定性
没有描述。
新！!: 直觉类型论和可判定性 · 查看更多 »
多元组
多元組泛指有限個元素所組成的序列。在數學上及計算機科學上分別有其特殊的意義。 数学上，n元组或多元组是对象个数有限的序列。元组由三部分组成：边界符、分隔符和元素。通常采用的边界符是小括号“(\)”，分隔符是逗号。 多元组被数学家用来描述包含特定部件的数学对象。例如，有向图被定义成一个二元组（V, E），这里V是节点的集合，E是V × V的子集，表示边。 在類型論中，多元組與重類別相關。.
外延
一个想法或（语言）表达的外延由它所适用于的事物构成；它是相对于内涵的。这个一般概念来自语义学，也适用于一些其他领域。.
存在量化
在谓词逻辑中，存在量化是对一个域的至少一个成员的性质或关系的论断。使用叫做存在量词逻辑算子符号∃来指示存在量化。 它相对于声称某些事物对所有事物都为真的全称量化。.
新！!: 直觉类型论和存在量化 · 查看更多 »
实数
实数，是有理數和無理數的总称，前者如0、-4、81/7；后者如\sqrt、\pi等。实数可以直观地看作小數（有限或無限的），它們能把数轴「填滿」。但僅僅以枚舉的方式不能描述實數的全體。实数和虚数共同构成复数。 根据日常经验，有理數集在數軸上似乎是「稠密」的，于是古人一直认为用有理數即能滿足測量上的實際需要。以邊長為1公分的正方形為例，其對角線有多長？在規定的精度下（比如誤差小於0.001公分），總可以用有理數來表示足夠精確的測量結果（比如1.414公分）。但是，古希臘畢達哥拉斯學派的數學家發現，只使用有理數無法完全精確地表示這條對角線的長度，這徹底地打擊了他們的數學理念；他們原以為：.
安德雷·柯爾莫哥洛夫
安德雷·尼古拉耶維奇·柯爾莫哥洛夫（俄语：Андре́й Никола́евич Колмого́ров，英语：Andrey Nikolaevich Kolmogorov，），俄国數學家，主要研究概率論、算法信息論、拓撲學、直觉主义逻辑、紊流、经典力学和計算複雜性理論，最為人所道的是對概率論公理化所作出的貢獻。他曾說："概率論作為數學學科，可以而且應該從公理開始建設，和幾何、代數的路一樣"。.
新！!: 直觉类型论和安德雷·柯爾莫哥洛夫 · 查看更多 »
不交并
在集合論，一組集合的不交并指的是一種修改過的并集運算，除了普通的并集，還標記了元素的來源。不交并還有另一個意義，指的是兩兩不交的集合的并集。.
交換律
交換律(Commutative property)是被普遍使用的一個數學名詞，意指能改變某物的順序而不改變其最終結果。交換律是大多數數學分支中的基本性質，而且許多的數學證明需要倚靠交換律。簡單運算的交換律許久都被假定存在，且沒有給定其一特定的名稱，直到19世紀，數學家開始形式化數學理論之後，交換律才被聲明。.
依赖类型
在计算机科学和逻辑中，依赖类型（或依存类型，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*。.
新！!: 直觉类型论和依赖类型 · 查看更多 »
命题
在现代哲学、逻辑学、语言学中，命题是指一个判断（陳述）的语义（實際表達的概念），這個概念是可以被定義並觀察的現象。命题不是指判断（陳述）本身。当相異判断（陳述）具有相同语义的时候，他们表达相同的命题。例如，雪是白的（汉语）和 Snow is white（英语）是相異的判断（陳述），但它们表达的命题是相同的。在同一种语言中，两个相異判断（陳述）也可能表达相同命题。例如，刚才的命题也可以说成冰的小结晶是白的，不過，之所以是相同命题，取決於冰的小结晶可視為雪的有效定義。 通常，命題是指閉判斷，以區別於開判斷，或謂詞。在這種情況下，命題不是真的就是假的。哲學學派邏輯實證主義支援這一命題的概念。 一些哲學家，諸如約翰•希爾勒，認為其他形式的語言或行為也判定命題。是非疑問句是對命題真值的詢問。道路交通標誌不通過語言和文字也表達了命題。使用陳述句也可能給出一個命題而不判定它，例如，在當老師請學生對某個引用發表意見的時候，這個引用就是一個命題（即它有語義）而這個老師並沒有判定它。在上一段中，只給出了命題雪是白的，但沒有判定它。.
命题逻辑
在邏輯和數學裡，命題演算（或稱句子演算）是一個形式系統，有著可以由以邏輯運算符結合原子命題來構成代表「命題」的公式，以及允許某些公式建構成「定理」的一套形式「證明規則」。.
新！!: 直觉类型论和命题逻辑 · 查看更多 »
哲学家
#重定向 哲學家.
内涵
内涵（Intension或connotation）是指一個符號、词語、或句子的意义或特征，多半是用定义的方式表达。 内涵经常与外延一起讨论。内涵称谓一个词能描述的所有可能的事物的集合。相反的，外延或指称（denotation）称谓一个词实际上描述的所有真实的事物的集合。例如，“轿车”的内涵是所有可能的轿车（包括巧克力造的轿车）。但是“轿车”的外延是所有真实的（过去现在和未来）轿车，这可能会总计为数以亿计的轿车，但可能不包含任何巧克力造的 mile-high 轿车。.
函数空间
在数学中，函数空间是从集合X到集合Y的给定种类的函数的集合。它叫做空间是因为在很多应用中，它是拓扑空间或向量空间或这二者。.
新！!: 直觉类型论和函数空间 · 查看更多 »
函數程式語言
函數式編程（functional programming）或称函数程序设计，又稱泛函編程，是一種編程典範，它將電腦運算視為數學上的函數計算，並且避免使用程序状态以及易变物件。函數程式語言最重要的基礎是λ演算（lambda calculus）。而且λ演算的函數可以接受函數當作輸入（引數）和輸出（傳出值）。 比起指令式編程，函數式編程更加強調程序执行的结果而非执行的过程，倡导利用若干简单的执行单元让计算结果不断渐进，逐层推导复杂的运算，而不是设计一个复杂的执行过程。.
新！!: 直觉类型论和函數程式語言 · 查看更多 »
全称量化
在谓词逻辑中，全称量化是尝试形式化某个事物（逻辑谓词）对于所有事物或所有有关的事物都为真的概念。结果的陈述是全称量化后的陈述，我们在谓词上有了全称量化。在符号逻辑中，全称量词（典型的"∀"）是用来指示全称量化的符号。.
新！!: 直觉类型论和全称量化 · 查看更多 »
BHK释义
在数理逻辑中，直覺主義邏輯的布勞威爾-海廷-柯爾莫哥洛夫释义或BHK释义是由魯伊茲·布勞威爾、阿蘭德·海廷和独立的由安德雷·柯爾莫哥洛夫提出的。它有时也叫做可实现性释义，因为有关于斯蒂芬·科尔·克莱尼的可实现性理论。.
新！!: 直觉类型论和BHK释义 · 查看更多 »
Coq
Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的（certified）程序。Coq 的理论基础是归纳构造演算（calculus of inductive constructions）、一种构造演算（calculus of constructions）的衍生理论。Coq 并非一个自动化定理机器证明语言；然而，它提供了自动化定理证明的策略（tactics）和不同的决策过程。 Coq 同时还是一个依赖类型的函数式编程语言。它由法国PPS实验室的PI.R2团队研究开发，该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 Gérard Huet、Christine Paulin 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。 单词 coq 在法语中意为“公鸡”，此命名体现了法国在研究活动中使用动物名称命名工具的传统。 最初，它被简单地称作 Coc，意即构造演算（calculus of constructions）的缩写，同时也暗含了 Thierry Coquand（与 Gérard Huet 共同提出了前述的构造演算）的姓氏。 Coq 自身提供了一套规范语言 Gallina （gallina 在西班牙语中意为“母鸡”）。使用 Gallina 书写的程序具有规范化性质——它们总是会终止。此性质使之避开了停机问题 。同时，这也使得 Coq 语言本身并非图灵完全。.
笛卡儿积
在数学中，两个集合X和Y的笛卡儿积（Cartesian product），又称直积，在集合论中表示为X × Y，是所有可能的有序对組成的集合，其中有序對的第一个对象是X的成员，第二个对象是Y的成员。 舉個實例，如果集合X是13个元素的点数集合，而集合Y是4个元素的花色集合，则这两个集合的笛卡儿积是有52个元素的标准扑克牌的集合。 笛卡儿积得名于笛卡儿，因為這概念是由他建立的解析几何引申出來.
新！!: 直觉类型论和笛卡儿积 · 查看更多 »
等价类
在数学中，假設在一个集合X上定義一个等价关系（用 \sim來表示），则X中的某個元素a的等价类就是在X中等价于a的所有元素所形成的子集: 等价类的概念有助于从已经构造了的集合构造新集合。在X中的给定等价关系 \sim的所有等价类的集合表示为X/ \sim并叫做X除以\sim的商集。这种运算可以（实际上非常不正式的）被认为是输入集合除以等价关系的活动，所以名字“商”和这种记法都是模仿的除法。商集类似于除法的一个方面是，如果X是有限的并且等价类都是等势的，则X/ \sim的序是X的序除以一个等价类的序的商。商集被认为是带有所有等价点都识别出来的集合X。 对于任何等价关系，都有从X到X/ \sim的一个规范投影映射\pi，给出为\pi(x).
简单类型λ演算
单类型 lambda 演算(\lambda^\to)是连接词只有 \to (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、陪积或自然数(系统 T)甚至完全的递归(如PCF)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。.
新！!: 直觉类型论和简单类型λ演算 · 查看更多 »
类型论
在最广泛的层面上，类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上，它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的，并在伯特兰·罗素和阿弗烈·诺夫·怀海德的《数学原理》中起到重要作用。 在计算机科学分支中的编程语言理论中，类型论提供了设计分析和研究类型系统的形式基础。实际上，很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究，尽管有些人把它限制于对更加抽象的形式化如有类型lambda演算的研究。.
类型检查
#重定向 類型系統.
新！!: 直觉类型论和类型检查 · 查看更多 »
系统F
系统F，也叫做多态lambda演算或二阶lambda演算，是有类型lambda演算。它由逻辑学家Jean-Yves Girard和计算机科学家John C. Reynolds独立发现的。系统F形式化了编程语言中的参数多态的概念。 正如同lambda演算有取值于（rang over）函数的变量，和来自它们的粘合子（binder）；二阶lambda演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断 这里的α是类型变量。 在Curry-Howard同构下，系统F对应于二阶逻辑。 系统F，和甚至更加有表达力的lambda演算一起，可被看作Lambda立方体的一部分。.
编程语言
编程语言（programming language），是用来定义计算机程序的形式語言。它是一种被标准化的交流技巧，用来向计算机发出指令。一种计算机语言让程序员能够准确地定义计算机所需要使用的数据，并精确地定义在不同情况下所应当采取的行动。 最早的编程语言是在電腦發明之前產生的，當時是用來控制及自動演奏鋼琴的動作。在電腦領域已發明了上千不同的编程語言，而且每年仍有新的编程語言誕生。很多编程語言需要用指令方式說明計算的程序，而有些编程語言則屬於宣告式編程，說明需要的結果，而不說明如何計算。 编程语言的描述一般可以分為及語義。語法是說明編程語言中，哪些符號或文字的組合方式是正確的，語義則是對於編程的解釋。有些語言是用規格文件定義，例如C語言的規格文件也是ISO標準中一部份，2011年後的版本為ISO/IEC 9899:2011，而其他55語言（像Perl）有一份主要的文件，視為是。.
新！!: 直觉类型论和编程语言 · 查看更多 »
真值
在逻辑中，真值（truth value），又稱逻辑值（logical value），是指示一个陈述在什么程度上是真的。在計算機編程上多稱做布林值、布爾值。 在经典逻辑中，唯一可能的真值是真和假。但在其他逻辑中其他真值也是可能的：模糊逻辑和其他形式的多值逻辑使用比简单的真和假更多的真值。 在代数上说，集合形成了简单的布尔代数。可以把其他布尔代数用作多值逻辑中的真值集合，但直觉主义逻辑把布尔代数推广为海廷代数。 在topos理论中，topos的主客对象分类器接管了真值集合的位置。.
瑞典
典王国（Konungariket Sverige）是一个位于斯堪地纳维亚半岛的北歐国家，首都为斯德哥尔摩。西鄰挪威，东北与芬兰接壤，西南濒临斯卡格拉克海峡和卡特加特海峡，東邊為波罗的海與波的尼亞灣。即瑞典和與丹麦、德国、波兰、俄罗斯、立陶宛、拉脫維亞和爱沙尼亚隔海相望，於西南通过厄勒海峽大桥与丹麦相连。瑞典於1995年加入欧洲联盟。 瑞典面积为449,964平方公里，为北歐第一大国家，人口1000万，第三页 - 于2007年7月10日查阅。。64%的國土由森林覆蓋，人口密度低，只有都會地區人口密度較高，84%的人口居住在只佔国土面积1.3%的城市裡。瑞典是一个現代、自由與民主的高度发达国家，其公民享有高质的生活，政府亦非常注重环保。 瑞典是传统的铁、铜和木材出口国，其水资源也很丰富，但是石油和煤矿十分匮乏。隨著運輸以及通訊的進步，這些自然資源也能夠更大規模地從各地開採，尤其是木材與鐵礦。經濟自由與教育普及而讓瑞典開始歷經快速的工業化，並從1890年代開始發展製造業。20世紀瑞典成為一個福利國家。 1397年，瑞典與丹麦和挪威一起所組成了卡爾馬聯合（芬兰此時還是瑞典王國的一部分）。瑞典於16世纪初脫離卡爾馬聯合，並且與鄰國進行了多年的戰爭，尤其是與俄羅斯以及從未完全承認瑞典已經離開了卡爾瑪聯合的丹麥-挪威聯合。17世纪時瑞典藉由戰爭擴張領土，成為了強權國家，其領土面积為目前的兩倍之大。1809年瑞典失去了芬蘭，也不再具有強權地位。之后，瑞典沒有再參與過戰爭。 現今，瑞典被視為極力追求人权和平等的国家之一。瑞典二戰後設立許多社會福利的制度，並在聯合國開發計劃署的人类发展指数中通常名列前茅。.
直觉主义
在数学哲学和邏輯中，直觉主义（Intuitionism），或者新直觉主义（Neointuitionism ）（对应於前直觉主义（Preintuitionism）），是用人类的构造性思维活动进行数学研究的方法。也可翻译成直觀主義。 任何数学对象被视为思维构造的产物，所以一个对象的存在性等价于它的构造的可能性。这和古典的方法不同，因为根據古典方法，一个实体的存在可以通过否定它的不存在来证明。对直觉主义者來說，这是不正确的：不存在的否定不表示可能找到存在的构造证明。正因为如此，直觉主义是数学结构主义的一种；但它不是唯一的一类。 直觉主义把数学命题的正确性和它可以被证明等同起来；如果数学对象纯粹是精神上的构造，还有什么其它法则可以用作真实性的检验呢（如同直觉主义者所說的一样）？这意味着直觉主义者对一个数学命题的含义，可能與古典的数学家有不同理解。例如，说 A 或 B，对于一个直觉主义者，是宣称 A 或是 B 可以被「证明」，而非兩者之一「為真」。值得一提的是，只允許 A 或 非A 的排中律，在直覺主義邏輯中是不被允许的；因为不能假设人们总是能够证明命题 A 或它的否定命题。 直觉主义也拒绝承认的抽象概念；也就是说，它不把像所有自然数的集合或任意有理数的序列这样的无穷当作实体来考虑。这要求将集合论和微积分的基础分别重新构造为和构造主义分析。.
新！!: 直觉类型论和直觉主义 · 查看更多 »
直觉主义逻辑
觉主义逻辑或构造性逻辑是最初由阿蘭德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的证实性而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有存在性质，这使它还适合其他形式的数学构造主义。.
新！!: 直觉类型论和直觉主义逻辑 · 查看更多 »
非直谓性
一个数学定义是非直谓性的，如果它依赖于一个事物的集合，至少其中之一是它自身所定义的事物。换句话说，定义是自引用的。 罗素悖论是著名的非直谓性构造: “不包含自身作为成员的所有集合的集合”。悖论是这种集合是否包含自身 - 如果包含则根据它的定义它应当不是，而如果不是则根据它的定义它应当是。 但是，著名的数学家拉姆齐（Frank Plumpton Ramsey）争论说，非直谓性定义是绝对需要的。例如，"屋子里最高的人" 是非直谓性的，因为它依赖于它是其中元素的事物的集合，也就是在屋子中所有人的集合。对于数学，一个非直谓性定义是一个集合中最小元素，它被形式定义为: y.
新！!: 直觉类型论和非直谓性 · 查看更多 »
谓词逻辑
在数理逻辑中，谓词逻辑（Predicate logic）是符号形式系统的通用术语，比如一阶逻辑，二阶逻辑，多类逻辑或无穷逻辑等等。.
新！!: 直觉类型论和谓词逻辑 · 查看更多 »
鲁伊兹·布劳威尔
鲁伊兹·艾格博特斯·杨·布劳威尔(Luitzen Egbertus Jan Brouwer，多写作L.)(）是一位荷兰数学家和哲学家。他是数学直觉主义流派的创始人，也在拓扑学，集合论，测度论和复分析领域有很多贡献。.
新！!: 直觉类型论和鲁伊兹·布劳威尔 · 查看更多 »
自然数
数学中，自然数指用于计数（如「桌子上有三个苹果」）和定序（如「国内第三大城市」）的数字。用于计数时称之为基数，用于定序时称之为序数。 自然数的定义不一，可以指正整数 (1, 2, 3, 4, \ldots)，亦可以指非负整数 (0, 1, 2, 3, 4, \ldots)。前者多在数论中使用，后者多在集合论和计算机科学中使用，也是 标准中所采用的定义。 数学家一般以\mathbb代表以自然数组成的集合。自然数集是一個可數的，無上界的無窮集合。.
蕴涵
蕴涵（implication或entailment）在命题逻辑和谓词逻辑中用来描述在两个句子或句子的集合之间的联系。.
良基关系
在数学中，类 X 上的一个二元关系 R 被称为是良基的，当且仅当所有 X 的非空子集都有一个 R-极小元；就是说，对 X 的每一个非空子集 S，存在一个 S 中的元素 m 使得对于所有 S 中的 s，二元组 (s,m) 都不在 R 中。 等价的说，假定某种选择公理，一个二元关系称为是良基的，当且仅当它不包含可数的无穷降链，也就是说不存在 X 的元素的无穷序列 x0, x1, x2,...使得对所有的自然数 n 有着 xn+1 R xn。 在序理论中，一个偏序关系称为是良基的，当且仅当它对应的严格偏序是良基的。如果这个序还是全序，那么此时称这个序为良序。 在集合论中，一个集合 x 称为是一个良基集合，如果集成员关系在 x 的传递闭包上是良基的。策梅洛-弗兰克尔集合论中的正则公理，就是断言所有的集合都是良基的。.
新！!: 直觉类型论和良基关系 · 查看更多 »
集合论
集合論（Set theory）或稱集論，是研究集合（由一堆構成的整體）的數學理論，包含集合和元素（或稱為成員）、關係等最基本數學概念。在大多數現代數學的公式化中，都是在集合論的語言下談論各種。集合論、命題邏輯與謂詞邏輯共同構成了數學的公理化基礎，以未定義的「集合」與「集合成員」等術語來形式化地建構數學物件。 現代集合論的研究是在1870年代由俄国数学家康托爾及德國数学家理察·戴德金的樸素集合論開始。在樸素集合論中，集合是當做一堆物件構成的整體之類的自證概念，沒有有關集合的形式化定義。在發現樸素集合論會產生一些後，二十世紀初期提出了許多公理化集合論，其中最著名的是包括選擇公理的策梅洛-弗蘭克爾集合論，簡稱ZFC。公理化集合論不直接定義集合和集合成員，而是先規範可以描述其性質的一些公理。 集合論常被視為數學基礎之一，特別是 ZFC 集合論。除了其基礎的作用外，集合論也是數學理論中的一部份，當代的集合論研究有許多離散的主題，從實數線的結構到大基数的一致性等。.
逻辑
邏輯（λογική；Logik；logique；logic；意大利语、西班牙语、葡萄牙语: logica），又稱理則、論理、推理、推論，是对有效推論的哲學研究。邏輯被使用在大部份的智能活動中，但主要在哲學、心理、学习、推论统计学、脑科学、數學、語義學、 法律和電腦科學等領域內被視為一門學科。邏輯討論邏輯論證會呈現的一般形式，哪種形式是有效的，以及其中的謬論。 邏輯通常可分為三個部份：歸納推理、溯因推理和演繹推理。 在哲學裡，邏輯被應用在大多數的主要領域之中：形上學/宇宙論、本體論、知識論及倫理學。 在數學裡，邏輯是指形式逻辑和数理邏輯，形式逻辑是研究某個形式語言的有效推論。主要是演繹推理。 在辯證法中也會學習到邏輯。数理邏輯是研究抽象邏輯关系和数学基本的问题。 在心理、脑科学、語義學、 法律裡，是研究人类思想推理的处理。 在学习、推论统计学裡，是研究最大可能的结论。主要是歸納推理、溯因推理。 在電腦科學裡， 是研究各种方法的性质，可能性，和实现在机器上。主要是歸納推理、溯因推理，也有在歸納推理的研究。 从古文明开始（如古印度、中國和古希臘）都有對邏輯進行研究。在西方，亞里斯多德將邏輯建立成一門正式的學科，並在哲學中給予它一個基本的位置。.
逻辑与
在逻辑和数学中，逻辑合取或逻辑与或且是一个二元逻辑運算符。如果其两个变量的真值都为“真”，其结果为“真”，否则其结果为“假”。.
逻辑非
逻辑非是布尔代数中一种一元运算。它的运算结果是将运算元的真值--。 命题A的非可以有几种写法：.
逻辑运算符
在形式逻辑中，逻辑运算符或逻辑联结词把语句连接成更复杂的复杂语句。例如，假设有两个逻辑命题，分别是“正在下雨”和“我在屋里”，我们可以将它们组成复杂命题“正在下雨，并且我在屋里”或“没有正在下雨”或“如果正在下雨，那么我在屋里”。一个将两个语句组成的新的语句或命题叫做复合语句或复合命题。.
新！!: 直觉类型论和逻辑运算符 · 查看更多 »
逻辑或
逻辑或（logical or）又称逻辑析取（logical disjunction）、邏輯選言，是逻辑和数学概念中的一个二元逻辑算符。其运算方法是：如果其两个变量中有一个真值为“真”，其结果为“真”，两个变量同时为假，其结果为“假”。.
LEGO
#重定向 樂高.
新！!: 直觉类型论和LEGO · 查看更多 »
Per Martin-Löf
#重定向 佩尔·马丁-洛夫.
新！!: 直觉类型论和Per Martin-Löf · 查看更多 »
柯里-霍华德同构
柯里-霍華德对应是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（computational calculus）之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·加里和逻辑学家William Alvin Howard独立发现的。.
新！!: 直觉类型论和柯里-霍华德同构 · 查看更多 »
构造演算
构造演算(CoC)是高阶有类型 lambda 演算，这里的类型是一级值。因此在 CoC 内有可能定义从整数到类型、从类型到类型的函数，同从整数到整数的函数一样。CoC 是强规范化的。 CoC 最初由 Thierry Coquand 开发。 CoC 是 Coq 定理证明器早期版本的基础；它后来的版本建造在归纳构造演算之上，这是带有对归纳数据类型的天然支持的 CoC 扩展。在最初的 CoC 中，归纳数据类型必须模拟为它们的多态解构函数。.
新！!: 直觉类型论和构造演算 · 查看更多 »
有类型λ演算
有类型 lambda 演算是使用 lambda 符号（\lambda）指示匿名函数抽象的一种有类型的形式化。有类型 lambda 演算是基础编程语言并且是有类型的函数式编程语言如 ML 和 Haskell 和更间接的指令式编程语言的基础。它们通过 Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型 lambda 演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型 lambda 演算被看作无类型lambda演算的精细化。更现代的观点把有类型 lambda 演算看做更基础的理论，而把无类型 lambda 演算看作它的只有一个类型的特殊情况。.
新！!: 直觉类型论和有类型λ演算 · 查看更多 »
数学家
数学家是指一群對數學有深入了解的的人士，將其知識運用於其工作上（特別是解決數學問題）。數學家專注於數、數據、邏輯、集合、結構、空間、變化。 專注於解決純數學（基础数学）領域以外的問題的數學家稱為應用數學家，他們運用他們的特殊數學知識與專業的方法解決許多在科學領域的顯著問題。因為專注於廣泛領域的問題、理論系統、定點結構。應用數學家經常研究與制定數學模型.
数学归纳法
数学归纳法（Mathematical Induction、MI、ID）是一种数学证明方法，通常被用于证明某个给定命题在整个（或者局部）自然数范围内成立。除了自然数以外，广义上的数学归纳法也可以用于证明一般良基结构，例如：集合论中的树。这种广义的数学归纳法应用于数学逻辑和计算机科学领域，称作结构归纳法。 虽然数学归纳法名字中有“归纳”，但是数学归纳法并非不严谨的归纳推理法，它属于完全严谨的演绎推理法。事實上，所有數學證明都是演繹法。.
新！!: 直觉类型论和数学归纳法 · 查看更多 »
数学构造主义
#重定向 数学构成主义.
新！!: 直觉类型论和数学构造主义 · 查看更多 »
重定向到这里：
Martin-Löf 类型论，Per Martin-Lof，依赖类型论，归纳类型，直覺類型論，直觉类型理论。
