补充资料：递归可实现性

递归可实现性
recursive readability

5)c厂(，A)，当一且仅当。:(A〕l二0). 设A(x)是只含自由变元x的公式;如果n是自然数，则万是一个表示形式算术中数n的项. 6)er(日xA(x))，当一且仅当e=2”·3“且u;A(万). 7)。:(丫xA(幻)，当且仅当。是一个递归函数(recursive function)f的。jdel数，使得对任何自然数”，数.f(n)实现A恤). 一个闭公式F称为可实现的(realizable)，如果存在一个数。实现F.一个包含自由变元y、，…，y。，的公式A(y;，…，y。)可以看作是关于y，，…，夕。的一个谓词(“公式A(夕，，…，夕。1)是可实现的”).如果公式F在直觉主义算术(intuitio垃stic arithme-tic)中可由可实现公式推导出来，则F是可实现的(见!3」).特别地，每个直觉主义算术中可证明的公式是可实现的.存在一个公式A(x)，使得公式丫城A(戈)丫，A(劝)不是可实现的.对这个公式A(x)，公式门丫x(A(x)V门A(x))是可实现的，尽管它在经典意义下是假的. 每个在直觉主义谓词演算中可证的谓词公式U有这样的性质:由代换规则从U中得出的每个算术公式是可实现的.具有这种性质的谓词公式称为可实现的(reaUZable).已经证明(【4」)命题公式 ((二二D“D)〕份二DV，D))。 。(，勺DV门D)，是可实现的，其中D表示公式门PV门q，但在直觉主义命题演算(int吹io扭s康proP仍itional calculus)中不可推导.递归可实现性〔re叨亩e rea“zab正ty;Pe叼pcH业朋pea-皿3界MOC几} 在5.C.幻eene(见【IJ，[2])提出的部分递归函数(par回recurslve function)概念的基础上，算术公式的直觉主义语义的一种更精确定义.对每个闭的算术公式F，定义一个关系“自然数e实现公式F”;记为erF.根据公式F的结构，归纳定义关系erF. l)如果F是一个不含自由变元的原子公式，即F具有形式s二t，其中s和t是常项，则e;F，当且仅当e=0且项￡和t的值相同. 设A和B是不含自由变元的公式、 2)e;(’通%26B)，当且仅当e二Za·3“，其中a rA，b rB. 3)er(A VB)，当且仅当‘=2“·3“且a:注，或e=2’·3“且b r B. 4)er(AOB)，当且仅当e是一个一元部分递归函数中的C尚del数，使得对任何自然数a，“;A蕴涵职在点a有定义且职(a):B.

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