On Universes in Type Theory
On Universes in Type Theory
复制标题
论类型论中的宇宙
DOI：
10.1093/oso/9780198501275.003.0012
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Erik Palmgren
中科院分区：
文献类型：
--
作者：
Erik Palmgren
类型宇宙的概念是由Martin-Lof(1975)引入建构型理论的。根据类型理论中固有的命题即类型原则，这一概念扮演着两种角色。第一个是作为在某些类型构造下关闭的集合或类型的集合。第二个是作为一组建设性地给出的无穷大公式。本文讨论了类型论中的宇宙概念，并提出和研究了一些有用的扩展。我们假设熟悉类型理论，例如(Martin-Lof 1984)。宇宙已经有效地扩展了建构主义的领域。一个例子是构造性范畴理论，其中类型宇宙在处理大范畴方面扮演着Grothendieck集合宇宙的角色。一个更深刻的例子是Aczel(1986)对构造性集合论(CZF)的类型理论解释。这是通过将∈图编码成有序类型，并在宇宙的任意类型上进行分支来完成的。后一种概括性对于解释分离公理至关重要。宇宙和良序(W型)的引入提供了强大的证明论力量。这为证明理论家所研究的二阶算术的强子系统提供了建设性的理由(见Giffor和Rathjen(1994)和Setzer(1993)，关于一些早期结果，见Palmgren(1992))。目前看来，增加类型理论的证明论力量的最简单合理的方法是引入更强大的宇宙结构。在本文中，我们将给出两个这样的推广。除了有助于理解二阶算术的子系统和推动归纳可定义性的极限之外，这种结构还提供了大基数的直观类似(Rathjen等人。出现)。宇宙的第三个新用途是促进将经典推理纳入建构型理论。我们引进了一系列经典命题，并证明了“Π2-公式”的一个守恒结果。从经典证明中提取程序在类型理论中是很容易处理的。下一节介绍宇宙的概念。本文的中心部分是第三节，在这里我们引入了宇宙形成算子和在该算子下闭合的超宇宙。第4节总结了已知的情况
The notion of a universe of types was introduced into constructive type theory by Martin-Lof (1975). According to the propositions-as-types principle inherent in type theory, the notion plays two roles. The first is as a collection of sets or types closed under certain type constructions. The second is as a set of constructively given infinitary formulas. In this paper we discuss the notion of universe in type theory and suggest and study some useful extensions. We assume familiarity with type theory as presented in e.g. (Martin-Lof 1984). Universes have been effective in expanding the realm of constructivism. One example is constructive category theory where type universes take the roles of Grothendieck universes of sets, in handling large categories. A more profound example is Aczel’s (1986) type-theoretic interpretation of constructive set theory (CZF). It is done by coding ∈-diagrams into well-order types, with branching over an arbitrary type of the universe. The latter generality is crucial to interpret the separation axiom. The introduction of universes and well-orders (W-types) in conjunction gives a great proof-theoretic strength. This has provided constructive justification of strong subsystems of second order arithmetic studied by proof-theorists (see Griffor and Rathjen (1994) and Setzer (1993), and for some early results, see Palmgren (1992)). At present, it appears that the most easily justifiable way to increase the proof-theoretic strength of type theory is to introduce ever more powerful universe constructions. We will give two such extensions in this paper. Besides contributing to the understanding of subsystems of second order arithmetic and pushing the limits of inductive definability, such constructions provide intuitionistic analogues of large cardinals (Rathjen et al. to appear). A third new use of universes is to facilitate the incorporation of classical reasoning into constructive type theory. We introduce a universe of classical propositions and prove a conservation result for ‘Π2-formulas’. Extracting programs from classical proofs is then tractable within type theory. The next section gives an introduction to the notion of universe. The central part of the paper is Section 3 where we introduce a universe forming operator and a super universe closed under this operator. Section 4 summarises what is known