关于具有等式的Strong-Frege-3正集合论的相容性问题

理论计算机科学电子笔记169（2007）111-120www.elsevier.com/locate/entcs关于一个具有等式的Giacomo Lenzi贾科莫·伦齐1，2c/o比萨意大利比萨摘要本文讨论了一个由Hinnion于两年前提出的具有等式的正集合论Strong-Frege-3的相容性问题。 我们将展示“自然”模式，以满足Strong-Fr ege - 3的各种需求。关键词：正集合论，可拓性，理解，一致性。1介绍本文研究的是Strong-Frege-3的这一理论的独特之处在于，与类似的理论不同，理解图式中承认的公式不仅使用成员资格，甚至使用平等和不平等，而且两者都被经典地对待在[6]和[7]中，这一理论被错误地归于E.相反，第一个提出这个理论的人似乎是R。Hinnion，即使Weydert贡献了很多在该地区与他的论文[10].事实上，除了Brady [1]，Gilmore [2]和Skolem [8]等其他研究者的著作外，Hinnion本人的著作中也有一些受到Strong-Frege-3相同思想启发的理论，见[3]和[4]相反，[6]和[7]似乎是唯一致力于Strong-Frege-3本身的论文在这篇导言中，我们紧接着[7]定义了强弗雷格3理论Strong-Frege-3理论的名字来源于R.Hinnion，其解释如下：• 强：与另一个较弱的理论，称为弗雷格-3，其中不仅成员资格，甚至平等被视为三个价值相反;1由比萨大学应用数学系的合同支助2 电子邮件地址：lenzi@mail.dm.unipi.it1571-0661 © 2007由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2006.07.033112G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111• 弗雷格：为了纪念G。弗雷格，作者的第一个（虽然不一致）com-conception原则的集合，这是灵感的来源，这一（希望一致）的理论;• 3：因为成员资格是三值的，因为我们有两个关系∈和∈，相互排斥，并且给定两个集合x，y，我们有三种可能性：要么x∈y（意思是：x属于y），要么x∈y（意思是：x不属于y），或者两者都不成立，在这种情况下，x到y的成员资格假设为不确定的。值关于Strong-Frege-3理论的正式说明如下。我们称集合为Strong-Frege-3理论的内部对象该理论的形式语言是一阶语言，由两个二元谓词，∈（membership）和∈（bar-membership）组成，并包括等式谓词=。首先，我们有以下公理：公理1.（互斥）<$（x ∈ y<$x∈y）。这个公理意味着∈和∈是彼此的一种“弱否定”。然而，由于我们没有说明公理的反向箭头（这相当于说x∈y<$x∈y），我们没有先验地强加∈和∈是彼此的实否定;实际上，正如我们将看到的，这在强弗雷格-3中是可证明为假的在文献中，包含公理1的理论通常被称为这两种选择之间的主要区别是拓扑空间给出了自然的例子如果取复盖全域的闭集对，那么我们就可以得到仿协调模型（人们可能会想通过使用闭集不相交对的对偶概念来给出仿完全模型，但是这种方法对于Strong-Frege-3来说不够强大，尽管它对其他理论也有效，见[4]）。Strong-Frege-3中的一组是一种“双面奖牌”，因为它可以有零个或多个成员，以及零个或多个酒吧成员。无论如何，一个集合是由它的成员和条成员决定的，正如下面的公理所述：公理2. （外延）（t（（t ∈ x Particit ∈ y）（t∈x Particit ∈y）→ x = y。换句话说，任何两个具有相同成员和相同棒成员的集合是相等的.最后，我们给出了Strong-Frege-3的核心，即它的理解图式。这个想法是重复弗雷格• 我们缺少这一类别的信息，而没有这一类别;• 我们只考虑下面定义的• 当通过理解定义一个集合时，我们指定了它的成员和它的棒成员（因此，这个集合将由外延唯一地确定为了使这个想法形式化，让我们首先定义正公式：G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111113定义3.（正公式）正公式的集合PF是最小的∈，∈-公式集合，使得：• x∈y，x∈y，x=y，<$（x=y）对任意两个变量x，y都在PF中（这些是基本的正公式）;• 如果φ，φ在PF中，x是一个变量，那么φ，φ，φ xφ，φ xφ也在PF中。我们考虑二元x，y中的四种基本正公式：通过互斥，x∈y和x∈y处于相互弱否定的状态，或者由于它们都是正的，处于正的否定状态;而且x=y和<$（x=y）是彼此的（经典）否定，我们也可以考虑它们的对应关系为一个积极的否定，因为他们是积极的定义。因此，我们在基本的正公式之间有一个双射，称为正否定;通过归纳，这个双射可以自然地扩展到所有的正公式，我们在下面的定义中给出它定义4.（正公式的正否定）给出正公式φ，我们称φ的正否定为公式PN（φ），其中：• PN（x∈y）是x∈y，PN（x∈y）是x∈y，PN（x=y）是<$（x=y），PN（<$（x=y））x=y;• PN（φ）是PN（φ）PN（），并且PN（φ）是PN（φ）PN（）;• PN（xφ）是x. PN（φ），PN（xφ）是x. PN（φ）。我们写φ而不是PN（φ）。我们注意到，对于任何正公式φ，φ也是正公式，并且φ=φ。现在，由于在Strong-Frege-3中存在∈和∈，很自然地，将（某些）集合与（某些）公式配对。例如，给定两个公式φ（x）和φ（x），其唯一的自由变量是x，根据外延性，至多存在一个集合，其成员是那些享受φ的成员，其棒成员是那些享受φ的成员。当φ是一个正公式，且φ是φ时，这个集合通过以下公理模式存在，其中b是一个在φ中不自由的变量：公理5.（积极理解图式）A1，. . . . ，an. B. 你好（（x∈b）Participateφ（x，a1， . . ，an））<$（x∈bParticipateφ（x，a1， . . ，an）。我们用{x |φ（x，a1，. ，an）}上一个公理的集合b。我们称Strong-Frege-3为一阶理论，它的非逻辑公理是上面的公理1、2和5。所以，我们有互斥性，外延性，以及积极理解的图式。尚不清楚Strong-Frege-3是否一致。本文的目的是讨论Strong-Frege-3的相容性和它的一些有趣的片段2言论在本节中，我们重复在[6]中对Strong-Frege-3的评论。如前所述，Strong-Frege-3的一个独特之处在于它的集合具有114G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111因为它们有成员和棒成员，但有一个约束，即没有一个集合可以既是同一集合的成员又是棒成员虽然从表达的角度来看，正式公式似乎是一个非常差的类别，但理解图式暗示了许多集合的存在（通过外延性而唯一），例如：• V{x|x= x}，全称集合;对于每个集合x，我们有x∈V和<$（x∈V）;• thedualofVis{x|xx}，其中对于v y x，x∈{\displaystylex∈{\displaystyle x}};这个集合并不是真正的每个集合都是它的条成员• 对于每一个集合a，我们有单例{a}{x |x = a};它导致a ∈ {a}，并且b∈{a}，用于从a中提取b个数据;• 我们有补数a<${x|x∈a}，且x∈a当且仅当x∈a，x∈a当且仅当x∈a;• 我们有主超滤器Fa<${x|a∈x}，具有性质x∈Fa当且仅当a∈x，x∈Fa当且仅当a∈x;• 对于两个数据集a，b，我们有一个统一的数据库{x|x∈a<$x∈b}，suchthatx∈a<$b当且仅当x∈a或x∈b，且x∈a <$b当且仅当x∈a且x∈b;• 对于任何两个数据集a，b，我们都有一个完整的内部选择，|x∈a<$x∈b}，则x∈ a <$b当且仅当x ∈ a且x ∈ b，且x∈a <$b当且仅当x∈a或x∈b.并和交满足通常的等同性、交换性、结合性和分配性定律;特别是对于每一个k，我们可以通过以下方式定义任意的无序k-uplets：{a1，a2，.，ak}{a1}{a2}. {ak}。此 外 ， 请 注 意 ， 宇 宙 是 无 限 的 ， 例 如 。它 包 含 无 限 序 列 （ sn ）givenbyys0<$Vandndsn+1<${sn}。下面给出了一种有趣的集合第六章. （Cantorian sets）一个集合x称为Cantorian，如果它证明了y（y∈x<$y∈x）。我们注意到：V是Cantorian的;每个单例都是Cantorian的;并且并、交和补保持Cantorianity。因此，有一个无限的Cantorian集合的布尔代数。然而，也有非康托里亚集合：为了找到一些，我们考虑罗素的二律背反在Strong-Frege-3中变成了什么事实上，人们可能会想证明一个罗素式的二律背反，因此Strong-Frege-3的不一致性，通过使用集合R{x |x∈x}。G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111115实际上，从R的定义中，我们得到n.x∈RParticex∈x因此，取x=RR∈R参与R∈R但这并不矛盾;相反，根据公理1，我们只能得出结论，R既不是一个成员，也不是一个酒吧成员本身，因此它不是康托利亚人。还有更多。 现在考虑集合联系我们|R ∈ R}。从R的上述性质可以得出，R1没有成员，也没有bar-成员（并且它是具有这些性质的唯一集合，通过外延性）;因此，R1是3部分模型前面的评论表明Strong-Frege-3能够提供各种集合论构造。然而，正如我们所说的，Strong-Frege-3的相容性问题是开放的.所能做的是给出Strong-Frege-3碎片的模型在下面的小节中，我们将考虑一些有趣的片段和模型。3.1一个减去外延的理论模型Strong-Frege-3的一个相容片段由公理1和公理5给出，也就是说，该理论减去外延性公理有一个自然的首先，宇宙是由所有迭代理解的集合ICT给出的项，归纳定义为ICT=nICTn，其中：• ICT0为空;• ICTn+1是所有表达式{x|φ（x，t1，.，tk）}，其中φ（x，x1，.，xk）是具有k+1个自由变量的正公式，k≥ 0，且t1，.，t，k是ICT n的元素。我们指出，信息和通信技术是一套术语，而不是成套术语;因此，例如，{x |x = x，{x |x = x <$x = x}是信息和通信技术的不同要素。现在，ICT中的平等被定义为句法平等（因此上面的一对说明了模型不是扩展的）。最后，通过ICT上的一系列关系对∈α和∈α来归纳定义∈和∈，其中α是可数序数，并且：•0和0是空的;• 对于任何一个t，t1， . . . ，tkiinICT，welett∈α+1{x|φ（x，t1， . . . ，tk）}，其中，如果fφα（t，t1， . . ，tk），且ndt∈α+1{x|φ（x，t1， . . . ，tk）}，其中，如果fφα（t，t1， . . ，tk），116G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111其中φα和φα是通过将∈替换为∈α并将∈替换为∈α;• 若λ是极限序数，则∈λ≡α λ∈α且∈λ≡α λ∈α。我们注意到，∈α和∈α是α的单调函数，由于它们的定义域是ICT ，其 中hichiscountle，则cunte u我们注意到公理1成立，因为∈α和∈α对于每个α都是不相交的，这可以通过归纳法证明。对于理解图式，我们注意到，根据定义，我们有t∈{x|φ（x，t1， . . . ，tk）}ifandonlyift∈μ+1{x|φ（x，t1， . . . ...，tk）当且仅当φ（t，t1，...，tk），它给出了模式的前半部分（关于∈的模式）;另一半（关于∈）是类似的。3.2无量化器部分的模型另一种研究Strong-Frege-3相容性问题的方法是递归理论。在这一节中，我们用递归理论给出一个Strong-Frege-3的碎片模型，即无量子化器的碎片我们的想法是将一组Strong-Frege-3视为一个部分函数，（最多）值0和1，其中1表示成员资格，0表示酒吧成员资格。我们需要的是这些函数的单射枚举。我们按以下步骤进行。在这篇文章中，我们使用固定的整数集合和部分递归函数的整数集合，并设Wi=dom φi（因此，W是所有递归可重复的整数集合的编号）。设C是一类r.整数的集合C的枚举是部分递归函数f，使得C ={Wf（i）|i∈ ω}。此外，f称为单射的，如果对于任意两个指标i Wf（j）。我们有Wf（i）Friedberg在1958年证明了所有r.e. 有一个单射的enu，混合。这里我们想证明所有r. e的子类V01 集合，编码值为{0，1}的部分递归函数（相对于整数对的标准编码）。为了这个目的，我们回顾Kummer的一个引理，取自Wehner [9]：引理7.（Kummer [5]）设A是r.e.的可积类。整数的集合，可以划分为两个类A1，A2，使得：•A1的成员的每个有限子集在A2中有无限多个扩张;• A2是可注入的。那么A也是可内射的G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111117为了得到内射枚举，我们引入引理• A-01直升机• A1<${g ∈ V01|卡（g）是偶数或无穷小};• A2<${g ∈ V01|（g）是奇数。引理的假设是满足的。事实上，第一个V01有一个枚举，因为我们可以设计一个二进制部分递归函数U，它对{0，1}中的一元函数是通用的（本质上，我们可以取U（i，j）= φi（j），除了当φi（j）是一个不同于0和1的整数时U（i，j）发散），现在可以从S-M-N定理获得枚举。此外，引理的第一个条件显然是满足的。让我们验证第二个条件，说集合A2是可内射的.我们可以写一个程序P，有两个输入i和n，其行为如下。我们知道，有限集合、对和整数对的有限集合可以用单个整数编码。因此，给定第一个输入i∈ω，程序P检查由i编码的对的有限集合g，并验证g是否确实是奇数基数值为0，1的函数（否则，P发散）。然后，P取第二个输入整数n∈ω，验证n是否在g的定义域中（否则它发散），在这种情况下，它输出g（n）。这个程序P是i的可计算函数，所以有一个部分递归函数f使得：• f（i）被定义当且仅当i编码A2的元素;• 当f（i）被定义时，我们有P（i，n）=Wf（i）（n）（其中Wf（i）被视为一组对，即作为一个函数）;• {Wf（i）|i∈ω}= A2（t是，f是A2的一个整数比）;• 如果f（i）和f（j）被定义，且A2的i f是单射的）。j，则Wf（i）/=Wf（j）（即枚举因此，根据引理，我们有一个类V01的单射枚举f01.让阿吉是函数的图形（视为一组整数）是Wf01（i）。以ω为论域，若<$i（j）= 1，则记为j∈i，若<$i（j）= 0，则记为j∈i，得到了∈，∈-语言的一个模型M.模型M验证了公理1，因为所有的矩阵i都是函数，验证了公理2，因为编号f是单射的。让我们对所有没有量化器的正公式验证公理5。事实上，让我们首先验证每个可能的原子的理解模式公式发生在一个quantier自由正公式。对于x=x（同真公式），理解项是唯一的下标i，使得i是常数函数1。对于x∈ f（未定义公式），项是指数i，使得fi是处处未定义的函数。对于x=a，其中a是任意参数，项是118G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111ωωω函数f，使得f（a）= 1，并且对于每个a / = b，f（b）= 0。对于x∈x，我们取函数使得（i）=i（i）。对于x∈a，我们取函数a。对于a∈x，我们取φ使得φ（x）=φx（a）。请注意，两边都是参数的等式和成员关系可以简化为真或假或未定义，因此不需要考虑它们前面的公式的可以通过观察来处理，如果实现公式φ，则1−实现φ。现在对于两个集合a，b的并集，我们可以取函数f，如果fa和fb中至少有一个是1，则取值1，如果fa和fb都是0，则取值0，否则定义。最后，通过德摩根法则，求并补的交集。相反，我们不能理解一般的量化正公式，主要是因为递归可量化集合在存在量化器下是封闭的，但在泛量化器下不是。3.3A在Strong-Frege-3中，我们有回想一下，Vω可以定义为最小集合，使得：• n ∈Vω;• 如果t，s∈Vω，则t∈ {s}也∈Vω。在Vω中，我们有一个关于平等和隶属的自然定义，由此产生的结构是几个集合论的模型（特别是那些不包括无限性公理的我们可以构造Vω的等价形式被定义为最小类，使得：• V，n，n ∈V（3）;在Strong-Frege-3中，我们称之为V（3），• 若t，s∈V（3），则t∈ {s}∈V（3），t∈ {s}∈V（3）。ω ω ω即使不假设整个Strong-Frege-3模型的存在，“copy” of V可以把上面的定义看作是一个定义，任期，并通过定义平等，成员和共同成员之间的条款以适当的方式。更确切地说，我们通过归纳定义了规范化项的类NT，NT=kN Tk，其中：• NT0只包含三个元素V，V，V，V;• NTk+1是NTkplusaltexpesiofforms：（{t1， . . . ，tn}）的最小值{tn+1， . . ，tn+m}，G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111119ωωω{t1，.，tn}，∗∩ co {t1,... ，tn}，{t1，. ，tn}，co {t1，. ，tn}，其中n（和m，如果存在的话）是正的， ti是NT k的不同元素，并且列表t1， . . ，tn（andtn+1. . . ，tn+mifpresent）与可能出现在项中的语法符号（例如<，<符号co）上施加的某种顺序是一致的;请注意，符号co旨在替换条，并且被引入以便具有线性项，<<<<<很容易订购。我们得到V（3）的每一项都等于唯一的规范化项，规范化项之间的相等只是语法上的相等，隶属度和共隶属度是自然的。 由标准化项sat-它满足Strong-Frege-3的公理1和2。此外，它还满足Strong-Frege-3的(note这是无量化因子片段的子片段，因为量化因子在等式中可以被消除）。顺便说一句，注意到V（3）的所有元素t都可以用正公式定义可能会有些意思，因为对于每个t，都有一个正公式φt（x），只有取x=t才能满足。事实上，x=V可以写成y.y∈x;同样，x=V可以写成y.y∈x;x=V可以用类似的技巧，NT的所有元素，因此V（3）的所有元素，都可以被定义。是证明这些是Strong- Frege-3中唯一可用正公式定义的集合。4一般情况剩下的问题是为完整的Strong-Frege-3理论寻找模型。让我们简单讨论一下这一点。通常，正集理论的模型是通过在具有然而，这种我们已经看到，Strong-Frege-3的无量化器部分有一个递归可重算的模型。然而，递归论方法也有其局限性，因为似乎没有一个超越递归可枚举的类是已知的没有重复的枚举，递归可枚举集对于存在量化是封闭的，但对于泛量化不是。120G. Lenzi/Electronic Notes in Theoretical Computer Science 169（2007）111ω第三种方法可以考虑像上面V（3）这样的项模型，但是成员资格对于包含不是单调的（因为存在等式和不等式）这一事实使得不可能公正地解决问题。具有简单的感应构造。也许一个更精确的准长期模型可以完成这项工作。引用[1] R. Brady，The Consistency of the Axioms of Abstraction and Extensionality in a Three-ValuedLogic，Notre Dame Journal of Formal Logic（4）12（1971），447-453.[2] P. Gilmore，无外延的部分集合论的一致性，在：纯粹数学研讨会论文集，美国。数学索科，Providence，Rhode Island，（2）13（1974），147[3] R. 因此，LeparadoxedeRusselldanslesveresi on spoitivesdelatherienvedesense mles，C. R. 一个cad。斯克岛 PARIS，T。 304，S'erieI，n. 12，1987，307-310。[4] R. [10]见《形式逻辑学报》（1）35（1994），15-40.[5] M. Kummer，Friedberg定理的一个简单的无优先级证明，理论计算机科学74（1990），249[6] G. Lenzi，WeydertSoc. 数学贝尔格（3）44（1992），311[7] G. Lenzi，Weydert的SF 3减去Leibniz规则的非平凡模型Soc. 数学 贝尔格6（1999），77-90.[8] 日《理解公理的研究》，圣母院，J。 Formal Logic（4）3（1963），162-170.[9] S. Wehner，“可计算枚举和重复问题”，博士。论文，西蒙弗雷泽大学，1995年。[10] E. Weydert，“如何近似经典逻辑中的朴素理解方案”，博士。论文，波恩大学，1989年。