(BI)[∀α∀n(A(α(¯¯¯n))∨¬A(α(¯¯¯n)))∧∀α∃nA(α(¯¯¯n)) ∧∀α∀n(A(α(¯¯¯n))→B(α(¯¯¯n))) ∧∀α∀n(∀mB(α(¯¯¯n)⋅m)→B(α(¯¯¯n)))]→B(ε).
这里 ε 代表空序列、·代表串联,BI代表Bar Induction,而下标D指的是谓词的可解性。A条形原则为直觉主义提供了一个树的归纳原则;它表达了一个关于可解码属性的铺展的基础性原则。这个原则的扩展,其中可解码性的要求被弱化了,可以从布劳威尔的工作中提取出来,但这里将省略。连续性和条形原则有时在一个公理中得到体现,称为条形连续性公理。
条形原则和连续性公理一节中提到的邻接函数之间有密切联系。设IK是归纳定义的邻接函数类,由所有常数非零序列λm.n+1组成,并且如果f(0)=0,并且λm.f(x⋅m)∈IK,对于所有x,那么f∈IK。语句K=IK,也就是邻接函数可以归纳生成的语句,等同于BID。
布劳威尔对条形定理的证明很了不起,因为它使用了假设证明的井然有序的特性。它是基于这样的假设:任何关于序列上的属性A是条形的证明都可以分解成一个井然有序的典范证明。尽管它在经典上是有效的,但布劳威尔对该原则的证明表明,在直觉主义中接受它为有效原则的理由与支持它在经典数学中的可接受性的论据有根本的不同。
3.7 选择公理(Choice axioms)
从建构的角度来看,选择公理的完整形式是不可接受的,至少在集合论的某些其他核心公理,比如扩展性(Diaconescu 1975)面前是如此。对于让 A 是一个不知道是真还是假的陈述。那么以下两个集合的成员资格是不可判定的。
X={x∈{0,1}∣x=0∨(x=1∧A)}
Y={y∈{0,1}∣y=1∨(y=0∧A)}
存在一个选择函数f:{X,Y}→{0,1}从X和Y中选择一个元素。X 和 Y 中选择一个元素,意味着 (A∨¬A)。因为如果f(X)≠f(Y),就说明X≠Y,并且ence ¬ A 而 f ( X ) = f ( Y ) 意味着 A . 因此,一个选择函数为 { X , Y } 不可能存在。
然而,有一些公理的限制是直觉主义可以接受的,例如可数选择公理,也被下面要讨论的半直觉主义接受为合法原则:
(AC-N)∀R⊆N×N(∀m∃nmRn→∃α∈NN∀mmRα(m))
这个方案可以有如下的理由。对前提的证明应该提供一种方法,即给定 m 提供一个数字 n 这样 m R n . 因此,该函数 α 在自然数上的函数 N 的函数可以逐步构建:首先是一个元素 m 0 被选中,以便 0 R m 0 的值,这将是 α ( 0 ) . 那么一个元素 m 1 被选中,使得 1 R m 1 的值,这将是 α ( 1 ) ,以此类推。
其他几个选择公理也可以用类似的方式进行论证。这里只提一个,即从属选择的公理:
(DC-N) ∀R⊆N×N(∀m∃nmRn→∀k∃α∈NN(α(0)=k ∧∀i≥0α(i)Rα(i+1))).
同样在经典数学中,选择公理也被谨慎对待,而且经常明确提到在一个证明中需要多少选择。由于从属选择公理与经典集合理论中的一个重要公理(确定性公理)是一致的,而完整的选择公理则不是,所以人们特别关注这个公理,而且一般来说,如果有选择的话,人们会试图将证明中的选择量减少到从属选择。
数学联邦政治世界观提示您:看后求收藏(同人小说网http://tongren.me),接着再看更方便。