补充资料：构造选择原理

构造选择原理
constructive selection principle

构造选择原理【~如由ve sele团佣prind川e;切鱿印y-灯~uoa6o外”四~1， MapKOB厚粤(Ma内vpr，ndple) 由A A.Mal〕K〔，B({11，[21)提出的构造数学(con-struCtivemathemati。)中的逻辑一哲学原理，其一般形式断言由某一描述给定的构造过程，如果它不是潜在无穷的(无界可扩展的)，那么该过程停止.在构造数学中常用与其等价的几种具体形式.1)设甲是正规算法(normal algorithm)，p为某字母表土的字，如果命题甲不能作用于尸是可驳的，则甲可作用于P，记为 一、一。!伞(P)〕’平(尸).2)在形式算术扭llthematic，fo皿al)中构造选择原理可由下列公式表小 丫:V*卜叭J、仁.、，川，玉·升伙、‘，刀}，其中7、.是一个原始递归谓词，使得Godel数为:的部分递归函数在x处有定义当且仅当刁y不(:，x，y)(见!3]).3)如果一递归可枚举集是非空的，则它包含某一兀素.4)设月是自然数的一个算法可验证性质.如果断言不存在满足A的数的命题是可驳的，则存在具有性质A的自然数，相应的逻辑形式为: Vx(A(X)岁别(*))〕〔，，〕x月(x)〕渺A妙，))· 有时构造选择原理特指这种形式，因为所要的数可在下列构造过程中选出二验证A(0);如果为真，则选O为所要的数;否则，验证A(l)，等等， 构造数学中可用的抽象系统的框架内可如下直观判断构造选择原理:如果一给定构造过程的潜无穷的不可能性是确定可证的，则该过程的停止，作为一步步执行该过程的结果是潜可达的.这样，在潜可实现性抽象内，基于构造选择原理可以断言构造对象(constructive obj-ect)(如，将正规算法作用于某字的结果)的存在性. 从经典逻辑看来，构造选择原理是绝对允许的，因为它是消除双重否定和排中律的一般规则的特例，应用这些逻辑规则可归结为在许多递归函数(比cu玲ivefunction)论的构造中的构造选择原理，这使这些构造在构造数学中也有用.由构造选择原理可以得到构造分析(句nstructive analysis)中的许多重要结果.特别是算法算子连续性定理和能行泛函到部分递归泛函(亦见构造度量空间(constructive metrie space))的可扩展性定理构造选择原理应用的另一领域是在构造语义中([4」).在构造选择原理在构造数学中作为一般原理之前，在不同的构造意义卜做了许多基于各种形式的该原理的研究.这里必须提到IIC.H。~B在1943年(见【51)得到的基本结果:假定对一儿公式A(x)，对每个n，A(n)丫，A(n)在构造形式算术中可推导，且三xA(x)在古典算术中可推导，则公式日、A(x)在构造算术中可推导.在I6)中，由MapKoB发展的构造语义新系统内可以判断构造选择原理 由于受构造数学初期结论影响，一些倡导者带保留地运用构造选择原理.构造选择原理也被直觉主义者所排斥，因为从直觉主义观点看来它不是充分可信的.另一方面，联系于直觉主义数学的许多分支，人们详细地研究了相应的表达构造选择原理的形式模式的系统之间的关系问题，特别地，证明了模式(2)，(4)是独立于直觉主义谓词演算，算术和分析的(见【2].【71，!81).

说明：补充资料仅用于学习参考，请勿用于其它任何用途。