直觉类型理论

直觉类型理论（又称构造类型理论，或马丁-勒夫类型理论）是一种类型理论，也是数学的另一种基础。所有的版本都保留了构造逻辑的核心设计，即使用依赖类型。

马丁-勒夫根据数学建构主义的原则设计了这个类型理论。建构主义要求任何存在证明都要包含一个证人。因此，任何关于存在大于1000的素数的证明都必须确定一个既是素数又大于1000的具体数字。直观类型理论通过内化BHK解释完成了这个设计目标。一个有趣的结果是，证明成为可以被检查、比较和操作的数学对象。信念类型理论的类型构建器是按照与逻辑连接词的一对一对应关系来构建的。例如，逻辑连接词被称为暗示().这种对应关系被称为库里-霍华德同构。以前的类型理论也遵循这种同构，但马丁-勒夫的类型理论是xxx个通过引入从属类型将其扩展到谓词逻辑的类型理论。类型理论直觉型类型理论有3个有限类型，然后用5个不同的类型构造器组成。与集合理论不同，类型理论不是建立在像弗雷格的逻辑之上的。因此，类型理论的每一个特征都是作为数学和逻辑的特征而承担双重职责。如果你不熟悉类型理论而知道集合理论，那么快速的总结就是。类型包含术语，就像集合包含元素一样。术语属于一种且仅属于一种类型。术语如计算（减少）到像4这样的典型术语。更多内容请参见类型理论一文。0类型，1类型和2类型有3个有限类型。0型包含0个术语。1型包含1个规范术语。而2类型包含2个规范术语。因为0类型包含0个术语，它也被称为空类型。它被用来表示任何不存在的东西。

它也可以写成{displaystyle/bot}，表示任何无法证明的东西。并代表任何无法证明的东西。(也就是说，它的证明不能存在。)因此，否定被定义为对它的一个函数。同样地，1类型包含1个典型术语，代表存在。它也被称为单位类型。它通常代表可以被证明的命题，因此，有时被写成最后，2类型包含2个典范术语。它代表两个值之间的明确选择。它用于布尔值，但不用于命题。命题被认为是1类型，可以被证明为永远没有证明（0类型），也可以不被证明。(在直觉类型理论中，排除中间法则对命题不成立)。

Σ-类型包含有序对。与典型的有序对（或2元组）类型一样，Σ类型可以描述笛卡尔乘积。Σ-类型比典型的有序对类型更强大，因为有依赖类型。在有序对中，第二项的类型可以取决于xxx项的值。例如，一对中的xxx项可能是一个自然数，第二项的类型可能是一个长度等于xxx项的向量。这样的类型将被写成。用集合理论的术语来说，这类似于集合的索引不相交联合。在通常的有序对的情况下，第二项的类型并不取决于xxx项的值。因此，描述笛卡尔乘积的类型是这里需要注意的是，xxx项的值。{displaystylen}，在这里必须注意，xxx项的值，n，并不取决于第二个项的类型。Σ-类型可以用来建立数学和其他学科中使用的更长的依赖类型的图元。