映射论与ZFC的关系及一致性证明

理论计算机科学电子札记73（2004）217-245www.elsevier.com/locate/entcs地图理论：从井基与反基ThierryVall'e1，2爱尔兰科克科克大学计算机科学学院摘要映射论是无类型兰姆演算的一个强大的扩展（只增加了几个项常数）。由于Klaus Grue，它被设计成计算机科学和数学的共同基础一阶逻辑和集合论的所有原始概念，包括真值、连接词和数量词、集合成员和集合相等，都被解释为术语。所有常见的集合论构造，包括归纳数据类型，都可以得到计算解释。现在，格鲁在[19]中，我们已经证明了可以设计一个替代版本，该版本考虑了非良基集，并允许对它们进行共归纳推理。这个新版本开辟了一条道路，以直接表示共归纳的数据类型和循环过程和现象在地图理论。在这篇文章中，我们给出了两个版本的映射论及其与ZFC的关系的平行介绍。 我们也给出了一个证明，他们的相对一致性方面的存在一个强不可及的基数。这些证明在κ-连续语义中进行，这是Scott连续语义（其中κ = ω）到任何正则基数κ的扩展关键词：映射论，反基础，余归纳，非类型λ-演算，集合论，κ-连续语义，互模拟1由本系博士后基金资助意大利乌迪内大学数学与计算机科学系2 电子邮件地址：tv1@cs.ucc.ie1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.08.010218T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217内容1介绍22地图理论概要52.12005年2.2语义学73MT9中的命题演算3.1λ-演算和命题演算的公理103.2非单调影响103.3命题演算的嵌入113.4λ-演算公理和命题12的满足性4地图理论中的谓词演算134.1量化域Φ134.2MT13中的常数ε和量化器4.3量化公理144.4解释一阶理论144.5满足M中的量化公理155在Map Theory中嵌入ZFC165.1在Map Theory嵌入ZFC − ext5.2MTF中的可拓性公理MTA216MTF24的感应原理7MTA24中AF A的可证明性7.1MTA25的共诱导原理7.2AxiomMTA-Deco258一个开放的问题：MTA-CoPrim27的一致性9结论28参考文献281介绍良基映射理论无类型λ-演算在计算机科学中有着广泛的应用，特别是在函数式编程语言的理论中。它是Church [3] [4]引入的原始系统的一致部分，以便成为可计算性理论和数学基础（函数和应用作为原始概念）。回到丘奇[9]无类型λ演算的一个方程扩展，称为映射理论，并表明它至少与ZFC+FA一样强大，其中FA表示T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217219- -关于我们通常的基础公理。文献[2]证明了ZFC+SI理论的相容性，其中SI无边界映射理论然而，Grue在过去的十五年里，人们可以观察到对集合论中反基础的兴趣越来越大。这种兴趣主要是由计算机科学的一些发展所激发的。事实上，在这一领域，许多对象和现象确实具有非良好基础的特征：循环过程，过渡系统，自然语言中的悖论等。有些人喜欢字符串，实数，形式级数。可能是无限的，只能通过部分和渐进的知识来近似。因此，很自然地使用包含足够的非良基集合的宇宙作为框架来为这些对象或现象提供语义。此外，使用经典的定义和归纳推理原则来定义和推理这些对象往往是不相关的。所有这一切使得一些计算机科学家和数学家，如R。米尔纳，巴特·雅各布斯，扬·鲁滕，丹尼尔·图里，玛蒂娜·莱尼萨... (see[14]，[15]，[11]，[16]，[17]，[12]，[13]）提出了一种新的更适合的方法，即定义和使用定义和共归纳的双重原则。根据这种方法，我们在[19]中设计了一个映射论的反基版本，它将被表示为MTA。这个新的方程理论允许对非良基对象进行量化，并给出了共归纳推理的形式化。在[19]中，我们证明了MTA相对于ZFC+SI是相容的，并且它至少与ZFC+AF A一样强大，其中AF A是F.Honsell和M. Forti在[6]和推广的P.Aczel在[1]下的以下形式：AF A：记住一个图只是一个有序对（a，b），其中a是一个集合，b是关于a的二元关系，并且：定义1.1函数d是图（a，b）的装饰，如果对所有x∈a，我们有：d（x）={d（y）：（x，y）∈b}从AF A，我们可以推导出一大类非良基集的存在性。例如，我们可以很容易地检查，为了 此外，装饰的唯一性（定义为：d（x）=）意味着这个自单例是唯一的。220T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217∈相关工作映射论是一个非常原始的系统，它在精神上与其他基于无类型λ-演算的极少数基础系统中的每一个都非常不同首先，它的原始常数和规则的数量保持得很低。其次，它对隶属关系的解释本质上是传统解释的对偶，在传统解释中，集合由其特征函数表示，并且 让我们回顾一下，这种传统的解释是对教会最初制度的解释，例如，也是对弗拉格-米希尔制度的解释。感兴趣的读者可以在[ 2 ]中找到地图理论和Flagg-Myhill系统之间更深入的比较Klaus Grue最近在[10]中设计了一个新版本的MTF，其中特别地，这个新版 本被S. Skalberg 在[18] 中在定 理证明器Isabelle 中实现 了MapTheory。然而，这个新理论的一致性证明仍有待提出。文章计划在这篇文章中，我们给出了MTF和MTA的平行介绍，以及它们与ZFC的关系。我们还在κ-连续语义的框架内给出了它们的一致性证明，这是Scott连续语义的推广（和弱化）在第2节中，我们将给出MTF和MTA的非正式介绍，以及它们的共同核心（将由MT表示）。 在第三、四、五节中，我们将相继给出三组公理和规则，它们分别允许命题演算在MT中嵌入，谓词演算在MT中嵌入，ZFC在MTF和MTA中嵌入。 第6节和第7节将专门用于MTF中FA和MTA中AF A的确认。最后，在第8节中，我们将讨论一个关于MTA的另一种公理化的公开问题。本文中关于MTF的所有结果的完整证明可在[9]和[2]中找到，关于MTA的结果可在[19]中找到部分4.4推广到所有一阶语言的类似结果[9]只涉及集合论，缺失的证明也可以在[19]中找到。T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217221⊆2地图理论概要MT、MTF和MTA的概要分为两部分。 在第一部分中，我们将介绍这两个理论的语法，第二部分将介绍它们在[2]和[19]中进行的一致性证明非正式讨论将使用2.1语法2.1.1MTF和MTA的语言MTF和MTA理论唯一可用的表达手段是用几个常数充实的λ演算的项之间的方程。对于MTF，这些常数是ε，T，if，ε，φ，我们不得不在其上添加对于M T A的con st“= stecA“。 所有由谓词演算（如真值、连接词和数量词）和集合论（如隶属度和等式）使用的概念都可以用λ演算的术语来翻译。特别地，布尔真由常数“T“表示布尔值False由每个λ-抽象λx.A表示，但项F=defλx.T将作为其规范表示。除了经典的真值True和False之外，映射论还从λ-演算中借用了一个额外的“真值”，即未定义的真值，用常数“λ "表示。其他常数的作用将在后面解释。在下面，他遇到了一个变量A，B，... . A、B、...... 将表示映射论的项的递归项和项的有限序列（包括emptys序列）。 A′的最小值将表示为dbylg（A′）。我们会-不受你的尊重，v，. ，x，y.. . 而u′，v′，. x′，y′。. 映射论和ZFC的变量和有限序列（我们假设它们都使用相同的可数变量集）。我们将表示为FV（B）（resp. F V（B<$）），则项B（resp. 序列B¯）。CriptB[x<$]将实现F V（B）x′和将意味着x′s没有任何重复。最后，B[C<$/x<$$>]表示将C<$的子空间修正为x<$的变量所得到的结果，并满足lg（C<$）=lg（x<$）。公式2.1AB<$=defAB1. Bn=def（. （AB1）. Bn），其中B<$=（B1，.，Bn）公式2.2A<$=B<$ab证明了方程（Ai=Bi）1≤i≤n的成立性，其中hn=lg（A<$）=lg（B<$）。符号2.3<$A = B意味着方程A = B是MTF和MTA的定理。我们将为下列定理指定ΔMTF或ΔMTA，222T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217→⊥只属于两种理论中的一种。2.1.2映射论ZFC在Map Theory中的嵌入分为两个步骤：(i) 将ZFC中的每一个MG都转化为一个G项。(ii) 对于ZFC的每个定理G[x]，我们可以证明：► φx→（Gstec[x<$]=T）其中，我们将选择一个等式，φx→（Gstec[x<$]=T）是一个简短的等式，其直观含义是：“If当G被关闭时，我们会看到Gstec=T。第二步是通过关联到定理的每个证明来执行的G [x <$]在Z F C中，给出了方程n φ x的一个解（Gstec[x<$]=T）inMapTeory. 此外，请注意，映射论的一致性意味着我们可以通过h<$φx→（Gstec[x<$]=T）和d<$φx→（<$stecGstec[x<$]=T）来重新生成（其中，是术语翻译<$G）。 下列术语将是有用的：定义2.4ZFC的定理G[x]通过MTF或MTAi检验► φx→（Gstec[x<$]=T）2.1.3MT、MTF概述 和MTA如前所述，MT是MTF和MTA的共同核心。 组成分为三组公理和规则。第一个公理，称为λ-演算公理和命题演算公理，包括通常的αβ-等价，并描述常数T和if的计算行为。 最后，它包含一个规则，称为Quartum Non Datur，允许在MT中嵌入命题演算。第二个公理称为谓词演算公理，本质上描述了常数ε的行为，并允许我们在MT中嵌入谓词演算。第三个是所谓的构造公理3。这些公理陈述了一些简单的闭包性质，“集合的宇宙”，它在语法上它们主要用于将ZFC嵌入MTF和MTA中。理论MTF除了MT的公理和规则外，还多了一条构造公理和一条规则。该公理表示为MTF-Prim，在MTF验证中起着核心作用《无限公理》（Axiom of Infinity）这条规则被称为归纳原理，就像集合论的类似物一样，被用作“推理”的原则。而且还3在本文中，这组公理不仅包括Grue的构造公理，而且包括文[9]中的Well1， 2，T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217223∈ D用于显示MTF中的相等性（反射性，对称性，传递性）。除了MT的公理和规则之外，MTA理论还有一个解释了我们被迫用前者取代后者的原因 在第8节。MTA理论也有一个称为共归纳原理的规则和一组称为等式公理的公理，它们表达了等式的通常性质（在MTF中使用归纳原理证明）。最后，MTA还有最后一个额外的公理MTA-Deco，它对于AF A的验证至关重要.2.2语义2.2.1λ-演算的κ-连续语义如前所述，[2]和[4]中MTF和MTA模型的构造[19]是在λ-演算的κ-连续语义的框架下完成的，这是Scott的（ω-）连续语义对每个正则基数κ的直接推广。κ-cpo（κ-完全偏序）、κ-紧和κ-连续函数的概念通常是从κ-定向子集的概念定义的。偏序集D的子集B是κ-定向的，如果对所有X∈B使得Card（X）κ，存在X在B中的上界。<为了模拟映射论中包含常数ε和φ的一些公理，必须处理特定的κ-cpos：κ-Scott域。一个κ-cpo D是一个κ-Scott整环，如果D的每个有界子集都有一个sup，并且如果每个元素u是u以下的k-紧元的集合的sup（这然后，集合是κ-定向的）。关于κ-连续语义的更多细节可以在[2]或[19]中找到。与ω-情形一样，κ-连续函数也是对某种拓扑连续的函数，称为κ-Scott拓扑。这种拓扑的开集称为κ-开集。记法2.5[D → E]κ将表示来自D到E，其中D和E是κ-cpos。以κ -连续函数为态射的κ-cpos和κ-Scott整环范畴是两个Carnival闭范畴（c.c.c.）。 这些范畴产生了λ-演算的模型，这些模型是它们的自反对象，换句话说，三元组（M，λ，A），其中M是κ-cpo（resp. aκ-Scott域），λ∈[[M → M]κ<$$> → M]κ，A∈[M <$→[M → M]κ]κ和A∈λ=id[M <$→M]κ。在下文中，自相关的κ-cpo（M，λ，A）将简单地用M表示。现在让我们回顾一下||封闭项的参数，224T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217M∈ ∈M →MnnMM⊥aκ-cpo，对于具有常数的扩展λ-演算，并且相对于这些常数的解释j：|= u，如果u ∈ M|= u if u ∈ M|= j（c）对于每个常数c|= j (c) for every constant c|= A（|一|）（|一个j|）|)|= λ（u ∈ M −→| A[ u/x]|）|)符号2.6当没有歧义时，|一|将被简单地表示为A。此外，我们写MA=B来表示M满足方程A=B，即对于x<$=FV（A，B）和allu<$∈Mlg（x<$），itistrue在ZFC中，|A[u<$/x<$]|为|B[u<$/x<$]|.公式2.7对于u，x<$∈M：ux<$由归纳法定义为usual，lg（x<$）∈ω，满足romux=defA（u）（x）.记法2.8u Φ = def{ux：x∈ Φ}，对所有u∈ M和Φ ∈ M。让我们还记得，函数λ允许我们定义一个κ-连续函数的序列（λn）n∈ω，它将[Mn→ M]κ的函数编码到M中，其中f或所有nω，u 和f[]k，wehaveλn（f）x<$=f（x<$）。 由λ1=defλ出发，用归纳法给出了λ（f）x = f（x）。2.2.2映射论直观地说，首先，映射论的模型M是单调函数F加上两个额外元素TM和M的空间，后者也是映射论的最小元素。. 这3个分区的对应于三个Map Theory的真值：False是函数的真值，True它由TM表示，Undefined由M表示。在[2]中定义的κ-前模型遵循这第一直觉，并且是最自然的反应性κ-cpos，可以丰富到映射论的模型中。特别地，正如我们稍后将看到的，每个κ-前模型满足"λ-演算和命题演算的公理和规则"组。这种κ-cpos的存在只需要指称语义的标准工具，最简单的是在[2]中构建的。定义使用以下符号。记法2.9对于M∈（M，λ，A）是自相关的κ-cpo，我们记为：1) FM，或简称F，集合{λ（f）：f ∈[M → M] κ}。2) ≤ M是M上的阶。3) M是M的最小元素。注2.10很容易证明，对于F J= defλxλy。（xy），我们有：F={u∈ M：FJu=u}={u∈ M：λx.ux=u}T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217225MMM∈∈/∈定义2.11一个κ-预模型是一个自反的κ-Scott域（，λ，A），使得：1)M=F<${M，TM}和F<${M，TM}=2) TM是M的一个极大元，而M是它之下的唯一元3) λ和A到F的限制是两个逆同构，κ-cposF和[M → M]κ。4) A（TM）=x<$→TM和A（M）=x→M注2.12F和{TM}是κ-cpoM的κ-开子集.表示法2.13当没有歧义时，TM和M将简单地用T和表示。2.2.3κ-预模型中的集合论域对于MTF和MTA的建模，我们从任何κ-预模型开始。 这两个模型之间的区别始于构造的两个适当子集，在本文中分别用ΦF和ΦA表示（定义5.11和5.12）。这些集合，一旦被充份的等式和等价关系所丰富（在第一种情况下表示为=F和F，在第二种情况下表示为=A和A），将分别是ZFC+FA和ZFC+AF A的模型;然而，这要求对于某些（强）不可达基数σ，κ> σ。地图理论的一个主要特点是它对隶属关系的解释。在第一个直观的近似中，我们通过以下方式定义Φ上的 特别地，从集合论的观点来看，T表示映射论中的空集。但是很容易表现出不同的u，v∈Φ使得uΦ =v Φ，因此，关系φΦ不是外延的（即，两个不同的组可以具有相同的我们将在5.2.2节中看到如何使用某种商来获得隶属度的充分和扩展的解释。3机器翻译中的命题演算直到本文的最后，我们将假设κ是某个固定的正则基数，M是κ-预模型。在本节中，我们给出了MT的第一组公理和规则，即然后，我们引入了一个关于一类方程的重要缩写，称为非单调隐式方程。226T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217M►►≡阳离子4.接下来，我们将展示如何将命题演算转换为MT术语。最后，我们给出了在任意κ-预模型M中满足上述公理和规则的证明。3.1λ-演算和命题演算除了通常的αβ等价公理和规则（我们在这里省略了），第一组包含五个公理方案，描述了常数T，T，if的应用行为，以及一个名为QuartumNon Datur的规则，它在语法上表示，分成三部分对于所有条款A、B、C：MT-Applic -TTB=T MT-Applic-B=MT-如果T B C=B，则选择1μ mMT-如果λx.A B C=C，选择2λMT-如果λB C=λ，选择3λ让我们回想一下FJ= defλxλy。（xy）。QNDIfA[T/x]=B[T/x]且 A[FJx/x]=B[FJx/x]且A[/x] =B[/x]则A=B注3.1利用αβ-等价的公理和规则，很容易证明：A [FJx/x] = B [FJx/x] iA[λy.S/x] =B[λy.S/x]，对于所有的抽象，选择λy.S.3.2非单调蕴涵方程的缩写将由“def“引入定义3.2：1) A：B=def（if AB）[4]为了简化我们的论述，这里提出的非单调蕴涵概念只是[9]中定义的概念的一个特例。T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217227∅2) A<$：B=defB，如果A<$=3）A<$：B=defA1：（A2：.. ：（An：B）.. ）ifA<$=（A1，..，An）备注3.3使用Select1可以很容易地检查出T：B=B。符号3.4（非单调含义）。A<$→BdefA<$：B=A<$：Tf→A→B的一个等式称为非单调蕴涵。它被称为蕴涵的原因是由下面的定理给出的，这是命题演算的前件式的类比。另一方面，它被称为非单调的，因为等式的特征函数不是单调的。相反，下面的定义3.7引入了一个术语，将“单调蕴涵”称为“单调蕴涵”，一个k-连续的，因此是单调的函数。Theorem3. 5（MP）A<$=T;A<$→BB=T某些非单调蕴涵对称为非单调等价。让我们介绍一个有用的缩写来写它们。记法3.6（非单调等价）A←→B→定义A→B;B→A3.3命题演算常量、if以及True和False（T和F），所有两个定义的术语，由富铁、惠铁，其中翻译命题演算中常用的连接词。这些项的定义可以很容易地从以下涉及变量项的β-约简的缩写中符号3.7对于所有变量x和y：1. F=defλx.T2. ！x=def（if x T T）3.！x<$=def！x1，.， ！xn，其中x′=（x1，...，xn）4. f=def（if x T F）5. <$stecx=def（ifxFT）6. xxf=def（ifxFF）7. xx= def（ifx！yy）8. xxx=def（ifxxxy！y）9. x惠stecy=def（ifx惠stecy）注3.8对于任意一个概率计算公式G[x]，我们可以用Gstec[x]表示，或简称为Gstec，它将该公式转换为MT 。ITIS228T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217►►⎧⊥⊥M如果u=，则为M使用上面的定义可以直接获得这个术语。本节中介绍的公理和规则（包括QND）的主要结果是下面的定理（使用术语“！”这是刚刚定义的）。Theorem3. 9如果G[x<$]是一个自适应的propositionalcalculu，则n为零！x<$→Gstec这是“”的直观含义！B= T是“B被定义”，即不是“B”。因为这很容易检查！T=T，就是这样。λx.A=T对于所有的A，x，定理的直观意义是：“If each variableofx是由u个真实值的y个值解释的结果或3.4λ-演算公理和命题演算公理在κ-预模型由于M是一个自反的κ-cpo，因此建立了αβ -等价的公理和规则模型.然后，取j（T）=TM和j（）=M，使用定义2.11.4，很明显：引理3.10对于所有的u∈ M，我们有M（Tu）= T和M（Tu）= T。我们现在需要给出一个常数的解释，如果满足MT-选择 公理。自然的方法是让j（if）=λ3（IF），其中IF是下面的函数（它的κ-连续性由注释2.12得出）。引理3.11从M3到M的函数IF，定义为：IF（u，v，w）=v if u=T如果v∈F是κ-连续的仍然需要检查是否满足QND。事实上，从注释2.10和定义2.11.3中可以清楚地看出，满足一个更强的性质，在[2]中称为强非基准量子（SQND），并表示如下。引理3.12（SQND）对于所有的κ-前模型M，我们有：M ={u∈ M：|F·J·U|= u}{T，}T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217229⎨⊥∃∀⎧如果n∈uΦMΦ4映射论4.1量化域Φ映射论的量化器和谓词演算的量化器之间的主要区别这个域在本节中用Φ表示，在语法中用常数φ表示，在M中用Φ的特征函数的代码来解释定义4.1我们将用χΦ表示以下函数，称为ΦM的特征函数，并在M上定义为：如果u∈Φ，则χ（u）=τT其他注4.2χΦ是κ-连续的，其中χ Φ是M的κ-开子集。事实上，χΦ只取两个值T，并且必须在语法中由以下公理表示：MT-Caract φx =！φx4.2MT中的常数ε和量化器量化器和通过常数ε在MT中转换，ε是希尔伯特选择算子的变体。这个常数表示下面定义的函数EΦ，相对于M上的某个固定选择函数ρ。定义4.3：EΦ（u）=ρ（Φ）ifuΦ <$F⎪⎩ρ({x∈Φ:ux=T})else我们将在4.5节中看到，Φ上的哪些条件意味着EΦ的κ-连续性，从而允许我们在 λ（EΦ）。 然后，量化器被定义为如下。定义4.4对于所有项A，令：1. εx.A=def（ε λx.A）2.你好A= def（λx. Aεx.A）3.你好A=defstecx. stecA230T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217用EΦ的编码来解释ε，我们得到了BUSTECANDBUSTEC，whichhicweke eeeexplicitforrBUSTEC（thedualresultholdinggforrBUSTEC）：Lemma4. 图5中的Iterstecx接口。A等于T、F或T，并且：1）M. A=Tiu∈Φ：MA[u/x]u∈Φ：MA[u/x]=T2）M. A=iu∈Φ：MA[u/x]=3) 我的天啊A=Fi <$$>u∈Φ：M<$A[u/x]∈F4.3量化公理这些公理表达了函数EΦ的一些有用的性质，特别是它的量化域是Φ。公理Quantif1是谓词演算的实例化规则的类似物：MT-Quantif1φ B，λstecx.A→A[B/x]MT-Quantif2ε x，A=εx. （φxεstecA）MT-Quantif3φ（εx. A）=100000。！一MT-Quantif4 stecx. A→φ（ε x.A）MT-Quantif5-stecx. A=100%。（φx：A）这些公理加到第一组公理上，有下面定理4.12作为主要推论。直观地说，这个定理表明，在机器翻译中嵌入谓词演算是可能的，只要翻译公式的术语有一个4.4解释一阶理论在本节结束之前，L将表示任何一阶语言。我们用PL表示L的谓词符号集，用FL表示L的函数符号集，用FL表示一阶L-公式集。给定一个解释θ，它使L的每个谓词或函数符号与映射论的一个闭项相联系，我们用θtec表示θ到FL的直接扩张，即.使用定义3.7获得的一个，四点四符号4.6Gstec（resp. Rstec）将是θstec（G）（resp. θ（R））。例4.7设G是公式Rx <$x（Rx<$Qx），其中R，Q∈PL是一元预测数. nθstec（G）=defGstec=defθstecx. （Rstecx）定义4.8θ强制确定PL，如果对所有R∈PL，我们有：► φx1，....，φx n−→！ （θ（R）x1... x n）T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217231►−→其中n是R的arity。定义4.9θ迫使量化域在FL如果对所有f∈FL，我们有：φx1，....，φx n φ（θ（f）x1.其中n是f的arity。符号4.10φx<$=φx1，.，φxn，其中rex<$=（x1，，xn）定义4.11：(i) 如果<$φx<$−→θstec（G），则θ使公式G[x<$]∈FL成立(ii) 如果θ使理论T <$F L的所有定理成立，则θ使理论T <$FL成立。定理4.12如果θ强迫PL的确定，也强迫在FL下的量化域的封闭，则对每个理论T <$FL：θ验证T它验证了T我们以两个基本的句法结果结束这一节，这两个结果本质上是从量化公理得出的。第一个问题对于证明φ x → φ stecz的方程是至关重要的。Gstec[x<$，z]，其中G[x<$，z]是该理论的一个理论我们在翻译。定理4.13（附录）φB=T;！（请参阅。A）=T;A[B/z]=T你好A=T定理m4.14（Gene）F或每个t∈A[x′]，我们有：φx<$→AE你好A=T。4.5满足M现在让我们回到我们的κ-前模型M。数量公理的满足预先假定了函数χΦ和EΦ对常数φ和ε的解释，因此，预先假定了χΦ和EΦ的κ连续性（Def.4.3和4.1）。我们已经知道χΦ是κ-连续的，而χ Φ是κ-开子的，设置（备注4.2）。E Φ的连续性要求在下面的引理中给出。记法4.15↑H = def{u：<$v∈H，v≤Mu}，其中H<$M。定义4.16设a为任意基数。我们会说，K M基本上是- 小，如果存在H<引理4.17设Φ <$M，如果Φ本质上是κ-小的，则EΦ是κ-连续的。本节的主要结果是下面的定理。232T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217CIMMM∈定义4.18如果Φ是κ-开的并且本质上是κ-小的，则Φ是一个量化域（对于谓词演算）。定理4.19若Φ ∈ M是一个量化域，φ，ε分别由函数χ Φ和E Φ（的编码）解释，则 满足量化公理。当然，在处理集合论时，我们会对“大”Φ感兴趣，然而，我们可以有不那么雄心勃勃的目标。例如，假设我们对解释皮亚诺在地图理论中的算术感兴趣在这种情况下，相关的量化域将是Φ ω= def{λx1.λx n.T：n∈ω}。它容易检验Φω对所有κ都是κ-开的，并且它本质上是κ-小的当且仅当κ > ω。一个更简单的可能的量化域的例子是ΦBool =def{T，F}的域，它是κ-开的，并且对于所有κ≥ω，本质上是κ-小的。5在映射论中嵌入ZFC这里我们假设ZFC用两个关系符号=表示，我们用ZFC−ext表示理论ZFC减去可拓性公理。首先，注意ZFC中可拓性公理的特殊地位。事实上，ZFC−ext的所有公理都表达了某些集合的存在性，而可拓性公理则表达了成员资格和相等性的性质。关系在第一小节中，我们将概述映射论中ZFC−ext公理的验证（在定义2.4的意义上）。在第二章中，我们将介绍MTF中成员和等式的翻译，MTA，我们将对可拓性公理的验证说几句话，这可以从这些翻译中得到证明5.1在映射论中嵌入ZFC−ext从映射论的观点来看，ZFC −ext的公理表达了宇宙在某些运算下的封闭性：Pairing，Power，Union。（可能0元，对于断言特定集合存在的公理，如空集公理或无限公理）。集合上的每一个通常的运算都对应于映射论的一个术语，称为集合构造函数。 与我们选择的公理化有关的集合构造函数的列表在[19，p.55]中给出。在本文中，我们只给出了三个基本的有用的例子，T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217233∈ ∈ ∈∈Singleton、P airing和Ordered-Pairing操作：例5.1：1) Sg=defλxλz.x（通常用K表示）2) P = defλxλyλz。（如果z x y）3) ，（P（Sg x）（P xy））请注意，项x，y=def，xy对应于Kurakowski在2.2.3节中介绍的论域ΦF和ΦA在集合构造子下是封闭的，这一事实通过非单调蕴涵在句法上表达出来这些方程在MTF和MTA中遵循一组公理，称为构造公理，它们表达了ΦF和ΦA的一些简单的闭包性质，并且从λ-演算的角度来看是自然的。在5.1节的其余部分，我们将首先陈述这些公理。然后，我们将简短地描述一个验证ZFC−ext公理的通用方法。接下来，我们将感兴趣的建设公理的满意度，M. 我们将以M内部的宇宙ΦF和ΦA的定义结束。5.1.1构造公理构造公理使用以下缩写：Curry=defλaλxλy.a（P xy）Y = defλf。（λx.f（xx）λx.f（xx））Prim = defλfλaλb。（Y λgλx. （if x a（f λz.g（x（bz）xstecAy= def（（stecAx）y），其中stecA是在MTA中转换的术语（参见下面的定义5.24）。Y项是著名的Curry术语（Primfa b）表示原始递归函数，其中a定义基本情况，f定义递归情况，b类枚举可用的破坏性/前导函数。构造公理：（MT-T）φT=T（MT-F）φF=T（MT-φ）φφ=φ（MT-ε）φλx.A=φλx.φA（MT-App）φu，φz→φ（uz）234T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217（MT-P）φu，φv→φ（Puv）（MT-Curry）φu→φ（Curry u）（MT-Diag）φu→φλx. （（ux）x）（MT-CInv）φu，φv→φλx.u（xv）（MT-Comp）stecx. φ（fx），φu→φλ x。f（ux）（MT F-Prim） Pastecx. φ（fx），φa，φb→φ（Primfab）（MT A-Infinity）（T∈stecAzstecu. （u∈stecAz<$stecSu∈stecAz））=TMTF的构造公理（分别为：MTA）由十个第一公理加上MTF-Prim（分别为）组成。 MTA-Infinity ）。 注意，公理MT-Diag，MT-CInv和MT-Comp取代了[9]中的公理C-M1和C-M2它们确实更简单，从λ-演算的角度来看更自然，并且同样强大（如[9]和[2]所示注5.2MTF-Prim 意味着MTF中无限性公理的有效性。在MTA中处理无限性的自然方法是用对偶公理MTA-CoPrim代替MTF-Prim。事实上，正如我们将在第8节中讨论的那样，我们被迫退回到MTA-Infinity。5.1.2映射论中ZFC−ext的一般解释方法所有关于ZFC−ext的公理都具有形式x<$z。H[z，x<$]，其中H是一个f或mulaZFC的。得到这样一个定理的验证的一般方法是展示一个集合构造函数cH，使得：1.（H）→φ（cHx<$）（通常：单位元ΦF（或ΦA）在以下条件下闭合2.<$φx<$$> →H选[cHx<$$>，x<$]（其中H选是H的翻译）然后，使用定理4.13和4.14，可以推导出：3.你知道的Hstec[z，x<$]=T例5.3对于配对公理，我们取cH=P，并证明：1. φx，φy→φ（P xy）52. φx，φy→（x∈stecPxy一个推论是：3. 你好，你好，（x∈stecz<$stecy∈stecz）=T[5]这里，MT-P的结果是直接的，但一般来说，这一步需要证明。T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217235M⊥ ∈⊆5.1.3满足构造公理为了对一些构造公理建模，我们需要假设存在一个强不可达基数。 所以我们假设是建立在满足ZFC + SI的宇宙中的。字母σ表示固定的不可达基数，我们假设M是κ-预模型，且κ > σ。我们还假设常数f、T和if的解释与3.4节和4.2节相同。在下文中，Φ M是一个量化域（在定义式4.18的意义上），我们假设φ和ε由χΦ和EΦ的代码解释。在本节中，我们将提出对Φ的一些要求，这将使我们能够对MTF和MTA的构造公理进行建模。记法5.4K<$→H ={u：<$x∈K，ux∈H}，对所有K，H <$M。注释5.5对于所有x<$∈Gω和n∈ω，我们将用yx<$n个由x <$的第n个元素组成的等式nce表示。 特别地，如果n=0，则n×n是空序列。定义5.6设G M：1. G0=def{u∈M：<$x<$$> ∈Gω，<$n ∈ω：ux<$n=T}2. G+=def{u∈M：<$x<$$> ∈Gω，<$n ∈ω：ux<$n/=<$}注5.7/G0G+和运算（）0，（）+相对于包含量递减.符号5.8O σ（G）表示G的所有本质σ-小且κ-开子集的集合。我们现在定义两个性质（取决于σ），GCP（一般闭包性质）和GCPA（抗地基一般闭包性质）：定义5.9设G≠ M，我们说G满足：1) GCP当G=<${O0<$→G：O∈Oσ（G）}2) GCPA当G=<${O+<$→G：O∈Oσ（G）}我们现在准备给出这一节的主要定理，它实际上包含了两个定理。第一个来自[2]，其结果将由ΦF满足。第二个是从[19]而来的，它的结果将由ΦA满足。本节的其余部分将用来评论这个定理。定理m5.10如果n∈/Φ3T，则n：1. 如果Φ满足GCP，并且如果Φ ≤ Φ0，则M满足构造公理（使用MTF-Prim）。2. 如果Φ满足GCPA且如果 Φ≠Φ+nM满足构造236T. Vallée/Electronic Notes in Theoretical Computer Science 73（2004）217⊥⊆0ααMF公理（使用MTA-Infini）。首先，我们注意到，φ∈/Φ 3T平凡地蕴涵MT-T和MT - T的满足，. 其余的讨论将涉及性质Φ Φ，它在[2]中被称为强归纳原理，并扮演两个不同的角色：1) 结合GCP，它允许我们证明MT-A