一种通用的构造性证明技术在一致空间的构造理论中的应用

理论计算机科学电子笔记120（2005）31-43www.elsevier.com/locate/entcs一种通用的构造性证明技术道格拉斯·布里奇斯1，2新西兰基督城坎特伯雷大学数学与统计系LuminitaVta3新西兰基督城坎特伯雷大学数学与统计系摘要在一致空间的构造理论中，出现了一种证明方法，其中排中律的弱形式的应用被纯粹的分析方法所规避。这种证明技术的本质保留字：统一的结构，构造性数学。1作者感谢新西兰皇家学会Marsden基金从1997年4月至2002年10月对他们的研究给予的大力支持;感谢新西兰皇家学会于2002年10月由Lumin颁发的新西兰科学技术博士后研究奖学金;感谢DAAD在论文撰写期间为D ouglasBridgesaGastprofessora tLudwig-最后，他们感谢杰里米·克拉克对论文早期版本提出的几项更正2电子邮件：d. math.canterbury.ac.nz3电子邮件：l. math.canterbury.ac.nz1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.06.03232D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页∈∈∈∈1介绍Apartness空间的理论，一个对应的经典理论的proximity空间，似乎有前途的基础建设4拓扑。在几篇涉及度量和一致分离空间的论文中，我们使用了一种似乎是一般证明技术的特别变体，我们现在概述一下我们有N =P<$Q，其中N是正整数的集合，集合P，Q的定义取决于某些附加假设。我们最终要证明n P。 我们首先使用额外的信息，例如一致空间之间某些映射的强连续性（见下文），证明n P最终保持5，否则n Q无限频繁。为了排除第二种选择，我们接着证明它蕴涵着排中律的一个弱形式，并且如果这个弱形式的排中律被加到直觉逻辑中，那么n∈Q是矛盾的经常地。从这一切可以得出，n最终∈P。在本说明中，我们将这些想法扩展成一个令人惊讶的强大的证明我们只需要对那个理论有最起码的了解，如在[13]中所发现的那样;但是为了帮助读者，我们将在第3节的开头给出一些基本的定义。2The我们的这些结果中的第一个是一个特别有建设性的结果，它消除了许多后续证明的刺痛，并且由于毕晓普所谓的有限全知原则（LPO）的建设性失败而成为必要：对于每个二元序列（λn）n1，要么λn= 0，要么存在n，则λn= 1。[4]我们所说的构造性数学是指具有直觉主义逻辑的数学;见[1，2，4，14]。5设A是一组正整数。如果存在N使得对所有n N n∈A，则我们说n最终或对所有极大的n，n∈A;如果我们能构造一个严格递增的正整数序列（n k）k1，使得对每个k，n k A，则我们说n无限经常地∈ A。[6]我们以前的一篇论文[7]讨论了一致空间理论中的证明技术这种技巧足够强，可以产生下面的定理3.3;但是，与[7]中提出的并随后在[8]中修正的要求相反，它不足以用于该论文中的其他两此外，它没有石原D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页33∈在它的递归解释中（用经典逻辑），LPO包含停机问题的可判定性（[4]，第3章）。引理2.1设S是一个非空集，H是S中序列s的集合，使得如果s H，则s的每个子序列都属于H。设T是S的子集，具有以下性质：如果s∈H，N=P<$Q，且对每个n∈Q，sn∈T，（1）则要么n∈P对所有n，要么存在n∈Q。 如果（1）成立，则要么n最终∈P，要么n无限频繁地∈Q。证据 根据我们的假设，我们可以不失一般性地假定存在 n1∈Q. 设λ0=λ1=0。利用相依选择，我们归纳地构造了一个二元递增序列（λk）k1和一个严格递增正整数序列（nk）k1，使得对于每个k> 1，• 若λk=0，则nk∈Q，且• 若λ k= 1 −λ k−1，则对所有n> n k−1，n ∈ P。为此，假设我们已经找到了nk−1的适用性质。德费恩PJ={j1：nk−1+j∈P}，QJ={j1：nk−1+j∈Q}，和sJ=.snk−1+j<$j1 .一、则根据我们的第一个假设， SJ∈ H，且N = Pj <$QJ。此外，如果j ∈QJ，则n k−1+ j∈Q，因此sJj∈T。应用我们的假设，将P，Q，s分别替换为PJ，QJ，SJ，我们可以看到，或者对于所有n> nk−1，n ∈P，在这种情况 下 ， 对 于 每 个 j1 ， 我 们 设 置 nk−1+j=nk−1+j ， 并 且 λk=1; 或 者 存 在nk>nk−1，并且nk∈Q，我们设置λk=0。这就完成了我们的归纳结构。现在让PJJ={k∈ N：λk= 0<$λk−1 = 1}，QJJ ={k∈ N：λk= 1−λk−1}，和sJJ=.snk−1k2.我们看到sJJ∈H，并且N =PJJ<$QJJ。此外，如果k∈QJJ，则n k−1∈ Q，且sJkJ= s nk−1∈ T。 应用我们的假设，P，Q，s，k被替换分别通过PJJ，QJJ，sJkJ，我们可以看到，要么k∈PJJ，对于所有k，要么有存在sk∈QJJ。如果tc为e，如果λj=1−λj−1，对于somej，则nj∈/PJJ，一个矛盾;其中λk= 0对于所有k，因此（nk）k1是严格的34D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页∈∈Q的元素的递增序列。在存在k∈QJJ的情况下，我们有n∈P对所有n> n k−1。Q我们的下一个引理可能看起来很奇怪，因为它表明在某些假设下，非构造性命题LPO成立。然而，它使我们能够使用LPO来排除引理2.1的结论中不需要的第二个选择。引理2.2在引理2.1的假设下，如果n∈Q无限频繁，则LPO成立。证据在Q中选择一个严格递增序列（nk）k1，注意对 所 有 k ， snk∈T。 考虑任意递增二元序列（λ k）k1。应用引理2.1，其中P，Q，s k被替换为PJ={k∈N：λk= 0}，QJ={k∈N：λk= 1}，关于S NK 分别地，我们发现，要么k∈PJ，对于所有k，要么存在k∈ QJ。Q命题2.3在引理2.1的假设下，设s∈H，设N =P<$Q，并假设对每个n ∈ Q，s n∈ T。还假设LPO <$$>（<$n<$k > n（k∈Q））。最终n∈P。证据 根据引理2.1，或者n最终P，否则NQ经常。在第二种情况下，引理2.2表明LPO成立，这在我们的最终假设看来是荒谬的。Q为了应用前面的定理，我们需要建立合适的S，H，T，并证明如果s∈ H，N = P <$Q，并且对于每个n ∈ Q，sn ∈ T，则要么n ∈ P，要么存在n∈Q。从命题2.3可以得出，n最终∈P。3连续性、收敛性和一致性设X是非空集，U，V是笛卡尔积的子集X×X。我们定义某些相关子集如下：D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页35UU<$V ={（x，y）：<$z ∈ X（（x，z）∈ U<$（z，y）∈ V）}，U1= U， U n+1= U<$U n（n = 1，2，. . ）的情况下，U−1={（x，y）：（y，x）∈ U}。我们说U是对称的，如果U=U−1。 X×X的对角线是n={（x，x）：x ∈ X}。X×X的子集的族U称为X上的一致结构或一致性，如果下列条件成立。U1IU中集合的每个有限交都属于U。IIX×X的每个包含U的成员的子集都在U中。U2U的每个成员都包含U的对角元和对称元。对于每个U∈U，存在V∈U使得V2<$U。对于每个U∈U，存在V∈U，使得<$x∈X×X（x∈U<$x∈/V）.对（X，U）--或者，不严格地说，单独的X--称为一致空间，U的元素是X的随从。为了清楚起见，我们有时用X来表示X上的一致结构。均匀空间是度量空间（X，ρ），其中唯一一致结构具有以下形式其中ε>0。{（x，y）∈X×X：ρ（x，y）≤ε}（2）条件U1，以及通过U2，U的每个元素都非空的事实，表明U是X × X上的滤波器。经典公理U4是超连续的（我们简单地取V=U）;但建设性地，它是必不可少的发展，理论一致空间的经典理论的一个很好的参考文献是[3]。一致空间（X，U）上的（一致）拓扑是指点x∈X的邻域基由以下集合组成的拓扑：U[x]={y ∈ X：（x，y）∈ U}（U ∈ U）。集合X上的拓扑τ被称为由一致结构U给出如果它与由U产生的一致拓扑重合。我们在一致空间（X，U）上定义了一个典范不等式：x/= y惠<$U∈ U（（x，y）∈/U）.36D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页/K∈注意，根据公理U1 II和U2，如果U∈ U，则U−1∈ U。因此，如果x/=y，则y/= x。此外，由于U包含x，如果x i = y，则<$（x = y）。因此，=具有两个性质，它们定义了构造性的不等式关系。数学反过来，X上的不等式以通常的方式导出X×X上的相关不等式。注意公理U4的一个明显更强的形式成立：对于每个U∈U，存在V∈U，使得X ∈X×X。x∈U<$ x∈CV<$，哪里CV={x∈X×X：v∈V（xx) }是V在X× X中的补数。对于每个正整数n，我们定义X的n -随行链为n -元组（U 1，.，U n）的随行，使得对于每个适用的k，U k是对称的，U2<$U k−1，并且X ∈X×X。x∈Uk−1。公理U3保证了对每个U∈U和每个正整数n存在一个n-链（U1，.，Un），其中U1= U.我们陈述两个关于一致空间的技术引理以供以后使用;这些引理出现在[7]的引理7和引理8中，并附有证明引理3.1设Y是一致空间，（an）n1，（bn）n1是Y中的序列，（V1，V2，V3）是Y的3-随行链，使得对每个n，（an，bn）∈ CV1. 则不可能对每个n，（a n，b k）V3对所有足够大的k.引理3.2假设LPO，设（a n）n1和（b n）n1是统一空间Y中的序列，设（V1，.，V4）是Y的一个4-随行链，使得对每个n，（an，bn）∈ CV1. 则存在正整数序列（nk）k1，使得（anj，bnk）∈CV4，对allj和k.我们说，一个一致空间（X，U）的两个子集A，B是分开的，我们写A da B，如果存在一个环境U，使得A×B<$CU={x∈X×X：<$y∈U（xy) }。X中的两个序列（xn）n1和（xjn）n1是最终闭的，如果对于X的每个环绕U，我们最终有（xn，xjn）∈U.从X到一致空间Y的映射f是D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页37Q• 强连续如果对X的所有子集A，B，f（A）daf（B）AdaB;• 一致序列连续，如果对于所有在X中最终接近的序列（xn）n1和（xJn）n1，序列（f（xn））n1和（f（xJn））n1在Y中最终接近。这两种连续性是一致连续性的弱形式。 我们的目标证明了下面的结果，其度量空间版本见[5]。定理3.3一致空间之间的强连续映射是一致序列连续的.我们的证明还需要更多的引理。引理3.4设X，Y是一致空间，f：X→Y是强连续函数，V是Y的一个环. 设（λ n）n1是增二元序列，（An）n1，（Bn）n1是X的子集序列，使得D对于X的每个环境U，存在N，使得对于每个nN，或者An×Bn=n，否则An×Bn与U相交;D如果λn=0，则An=0;并且D如果λn= 1−λn−1，则An对于所有k > n。Bnf（An）×f（Bn）<$CV，且Ak=<$则存在N使得λn= λ N，对所有nN.证据 注意，如果λ1= 1，则无需证明。写作A=n1A n，B=n1{Bn：λn= 1−λn−1}，我们看到f（A）×f（B）<$CV：因为如果x∈A，则存在n使得A=An，B=Bn，并且f（An）×f（Bn）<$CV。因此f（A）daf（B），因此，通过f的强连续性，存在X的一个环境U使得A×B<$CU。选择N，使得对于每个nN，要么A n×B n=n，要么A n×B n与U相交。或者λ N=1，因此λ n= 1，对于所有nN，否则λ N=0。在后一种情况下，如果λ m=1 −λ m−1，对于某个m > N，则A=A m/=，B=B m/=，且A×B与U相交。 这与我们对U的选择相矛盾;因此，对所有n N，λ n = 0。引理3.5设X，Y是一致空间，f：X→Y是强连续函数，V是Y的环境设S是空间X× X，H=. s∈ SN：<$U ∈ UX<$N<$nN（s n∈ U）<$，38D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页.Σ.Σ和T=.（x，xJ）∈ S：（f（x），f（xJ））∈ CV<$.如果s∈H，N=P<$Q，且对于每个n∈Q，s n∈T，则对于所有n，否则存在n∈ Q。证据对于每一个n写s n=（x n，xJn）。构造一个递增二元序列（λn）n1，使得• 若λn=0，则对所有k≤n，k∈P;• 若λ n= 1 −λ n−1，则n∈Q。我们可以假设λ1= 0。如果λ n= 0，则设A n= B n= λ n。如果λ n= 1 −λn−1，设A n={x n}和B n={xJn}，注意，当n ∈ Q时，我们有（x n，xJn）∈ T，因此f（A n）×f（B n）<$CV;也设A k=<$C = B k，对每个kn。现在考虑X的任何随从U。由于s∈H，存在ν使得对所有n ν（xn，XJn）∈U。对于每一个这样的n，如果λ n= 0或λ n−1= 1，则An×Bn=1。 另一方面， 若λn=1，则nAn×Bn={（ xn ， XJN）} <$U. 因此，引理3.4的假设成立。应用该引理，我们产生N，使得对于所有nN，λ n = λ N。若λN= 0，则对所有n，n∈P;若λ N= 1，则存在k≤n使得k ∈ Q.Q为了证明定理3.3，设S = X×X，并如前面的引理a那样定义H。设序列s（xn）n1，（xn，J）n1在X中是渐近闭合的，令s =（（xn，XJn））n1. 设V是Y的任意环境，构造一个5-链（V1，.，V5），其中V1= V. 德费恩P={n：（f（xn），f（xJn））∈V}，Q={n：（f（xn），f（xjn））∈CV2}，和T=.（x，XJ）∈ S：（f（x），f（XJ））∈ CV2<$.则N = P <$Q，s ∈ H，且对每个n ∈ Q，sn ∈ T。 从引理3.5和2.1可以得出，要么n最终∈ P，要么n无限频繁地∈ Q。假设n∈Q无限频繁，我们从引理2.2看到LPO成立。因此，根据引理3.2，存在正整数的严格递增序列（nk）k1，使得f（xnj），f（XJNK）∈CV5，对所有j，k。 写作A =. x nj：j1 π，B =. xJnk：k1k，我们看到f（A）×f（B）<$CV5，所以f（A）daf（B）在Y中。由于f是强连续 的，A da B 在X 中， 因此存在X 的一个环境U 使得 A×B<$CU。 但这是荒谬的，因为最终x nk，xJnk ∈ U。参照D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页39∈∈∈对于命题2.3，我们最终得出n P-，即（f（xn），f（xJn））V-。这就完成了证明。在[11]中表明，定理3.3是我们在不引入一个原则的情况下可以连续地产生的最好结果，该原则虽然在构造性数学的标准模型（直觉的，递归的，经典的）中有效，但似乎不能仅使用直觉逻辑和依赖选择来推导。在某些附加的假设下，定理3.3可以被加强以产生强连续函数f的一致连续性;参见[5]。从紧度量空间到度量空间的连续映射的一致连续性定理，用经典逻辑很容易地从定理3.3推出同样地，关于一致收敛的一个标准经典结果可以从命题2.3的下一个应用中得到。这需要更多的定义。设X为非空集，Y为一致空间，（φn）n1是Y X中的序列，且φ∈YX. 我们说（φn）近似收敛于φ，如果φ（A）da B<$$> N<$nN（φn（A）da B）;如 果 对 X 中 的 每 个 序 列 （ xn ） n1 ， 序 列 （ φ （ xn ） ） n1 和 （ φn（xn））n1最终接近，则（φn）一致序列收敛于φ 我们想证明下面的定理，它首先出现在[15]中。定理3.6设X是非空集，Y是一致空间，（φn）n1是Y X中逼近φ Y X的序列。 则（φn）一致序列收敛于φ。要做到这一点，我们需要引理3.4和3.5的对应物。引理3.7设X是非空集，Y是一致空间。 设（φn）n1是Y X中的一个序列，它逼近于φ∈Y X。设（xn）n1是X中的一个序列，V是Y的一个环. 设（λ n）n1是增二元序列，（An）n1，（Bn）n1分别是X，Y的子集序列，使得D如果λn= 0，则An =Bn=λ，并且D若λn= 1−λn−1，则An ={xn}，Bn={φn（xn）}，φ（An）×Bn<$CV，且对于所有k > n，A k= B k=。则存在N使得λn= λ N，对所有nN.证据 写40D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页.Σ--∈A=n1An，B = n1{B n：λ n= 1 −λ n−1}。如果x ∈ A，则存在n使得A = An={xn}，B = Bn={φn（ xn）}，且φ（An）×Bn <$CV。因此φ（A）×B<$CV，因此φ（A）daB。通过近似收敛，存在N使得φn（A）daB，对所有nN. 假设λ m= 1 −λ m−1，其中m > N。则A={xm}，B=φm（x m）φm（x m）da φm（x m），这是荒谬的。因此，λ n=λ N，对于所有nN.Q引理3.8设X是一个集合，Y是一致空间。设（φn）n1是Y X中的一个序列，它在φ∈Y X附近收敛. 设（xn）n1是X中的一个序列，V是Y的一个环.设P，Q是正整数集合，N= P <$Q，并设对所有n ∈ Q，（φ（xn），φn（xn））∈CV. 则要么n∈P对所有n，要么存在n∈ Q。证据 构造一个递增二元序列（λ n）n1，使得• 若λn=0，则对所有k≤n，k∈P;• 若λ n= 1 −λ n−1，则n∈Q。我们可以假设λ1= 0。如果λ n= 0，则设A n= B n=λ n。如果λ n= 1 −λn−1，设A n={x n}和B n={φn（x n）}，注意，当n∈Q时，我们有φ（An）× B n<$CV;也设A k=<$C = B k。 根据引理3.7，存在N使得λ n= λN，对于所有nN。若λ N= 0，则对所有n，n∈P;若λ N= 1，则对某些n≤ N，n ∈ Q。Q为了证明定理3.6，给定集合X和一致空间Y，设S = X×YX，H = SN。设（φn）n1是Y X中逼近φ Y X的序列，U是Y的一个环境，构造Y的一个环境的5-链（U，V1，V2，V3，V4）. 德费恩T=.（x，f）∈S：（φ（x），f（x））∈ CV1<$.设（xn）n1是X中的序列，s =（（xn，φn））n1∈H. 德费恩P={n：（φ（xn），φn（xn））∈U}，Q= n：（φ（xn），φn（xn））∈ CV1.应用引理3.8和2.1，我们看到，要么n最终∈P，要么n无限频繁地∈Q设Q中存在严格递增的正整数序列（nk）k1. 然后，根据引理2.2，LPO成立，所以我们可以D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页41∈∈∈应用引理3.2，εak=φ（xnk），bk=φnk（xnk），并且r=2，为了构造一个严格地增加一个p值序列e（ki）∞i=1的p值序列，.φ。x nkj，φnki.xnki∈CV4（i，j1）.（三）让A=，xnki：i1，，B=，φnkj.xnkjn：j1，.由式（3）可知，φ（A）daB。因此存在N使得φn（A）daB对于所有的N。特别地，对于所有iN，我们得到矛盾φ nki.x nki da φ nki.x nki.因此<$（<$n<$k> n（k∈Q）），因此，根据命题2.3，nP最终 即，（φ（xn），φn（xn））U表示所有极大的n。这就完成了证明。4石原在开创性的论文[12]中，Hajime Ishihara引入了两个引理，随后被称为Ishihara这些引理在[9]中的一个更一般的集合中进行了检验。最后，我们通过证明它们也与我们前面的证明技术有关来结束本文我们首先证明了石原的第一个技巧（[ 12 ]，引理1）的一个轻微的推广引理4.1设X是完备度量空间，x X，f是X到度量空间Y的强扩张映射. 设H是X中所有收敛于x的序列的集合，设α>0，定义T={y ∈ X：ρ（f（x），f（y））> α}.若（xn）n1∈H，N = P<$Q，且xn∈T，则要么n∈ P，要么存在n∈ Q.证据设（xn）n1∈H，N +=P<$Q，且对所有n∈ Q，xn ∈ T.构造一个递增二元序列（λn）n1，使得42D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页∈• 若λn=0，则对所有k≤n，k∈P;• 若λ n= 1 −λ n−1，则n∈Q。我们可以假设λ1= 0。 如果λ n= 0，设y n= x。 如果λ n= 1−λ n−1，则对所有k n，设y k= x n。则（ yn）n1是X中的柯西序列，因此收敛于极限y∈X。ρ（f（x），f（y））> 0或ρ（f（x），f（y））<α。在第一种情况下，由于f是强扩张的，我们有x/= y。 所以存在N使得xy N，由此得出λ N= 1，因此对于某些n≤ N，n ∈ Q。在ρ（f（x），f（y））<α的情况下，我们必须有λn= 0，因此n P，对于所有的;Q我们现在可以很容易地推导出石原命题4.2设X是完备度量空间，f是X到度量空间Y的强扩张映射，（xn）n1是收敛于极限x∈X的序列则对所有正的α，β和α β，ρ（f（xn），f（x））<β最终，否则ρ（f（x n），f（x））>α无限频繁。证据 取S = X，并让H和T被定义为引理的陈述4.1. 这个引理表明引理2.1的假设成立。将该引理应用于P={n：ρ（f（xn），f（x））<β}，Q={n：ρ（f（xn），f（x））> α}，我们立刻得到了想要的结果。Q因此，我们的引用[1] Beeson，M.J.，[2] Bishop，E.，和D. Bridges，“Constructive Analysis”，Grundlagen der Math.Wiss. 279，[3] Bourbaki，N.，“General Topology (Part 1)”, Addison–Wesley, Reading, MA,[4] 布里奇斯，D.，和F.李奇曼，[5] Bri d ges，D. ，和L. V.S.T.R&.D. Bri dge s，L. 《理论与计算科学》第12卷第0期（2005）31-43页43[6] Bri d ges，D. ，和L. 然而，Apartnesspacesafram o rkorcivetopolog y，Ann.PureAppl. Logic. 119（1[7] Bri d ges ， D. ， 和 L.V.A.P.O.F. S. P. C. A. P. C. C. A. P. C. C. SymbolicLogic68 （ 3 ）（2003），795[8] Bri d ges，D. ，和L. Vta，Corrigendum：Aproof-t e chni qu e i n un i f or m s p a c e t h e ory，[9] 布里奇斯，D.，D. van Dalen和H.石原，石原在Wetenschappen（Indag. Math.）国家安全局14（2）（2003）163- 168。[10] 布里奇斯，D.，F. Richman，and P. Schuster，A weak countable choice principle，Proc.Amer. Math. Soc.128（9）（2000），2749[11] Bridges，D. 、H. Ishihara，P. S.C. V[12] 石原，H.，构造性分析中的连续性与非连续性。Symbolic Logic56（4）（1991），1349[13] SCHUSTer ， P. ， L.VBridges ， Apartnesasareelationbenssubsets ， in ： Combinatorics ，Computabi l ityandLogi c（DMTCS'01的序言，Comst ana t an a ta n a t a，R om a n ia，2001年7月2日至6日Calude，M.J. Dinneen，S. Sburlan（eds.）），DMTCS Series17，Springer-Verlag[14] Troelstra，A.S.，和D.范达伦，“数学中的建构主义”（卷。I，II），北荷兰出版公司，阿姆斯特丹，1988年。[15] 我的天哪！，Pr oximalanduni form convergenceonapartness sspaces，Math. LogicQuarterly49（3）（2003），255