补充资料：形式算术

形式算术
arithmetic . formal

　　形式算术〔aritl。*康、拓rmal;ap“中Me~a加p~圈}，算术演算(ar一thmeti以}以!CUluS) 使初等数论形式化的一种逻辑一数学演算.最普通的形式算术语言包含常数0.变元，等号，函数符号十，·，(后续)和逻辑符号，由常数0和变元通过函数符号构造成项;特别地，自然数可用形如0”的项表示.原子公式是项的等式、其他公式是由原子公式通过逻辑连接词%26，丫，一，门，丫，已生成的.形式算术语言中的公式称为筹水兮不(arith-metlcal formul洲)形式算术的公设是谓词演算(pre-di以te calculus)〔古典或直觉主义的.取决于所讨论的形式算术)的公设和Peano公理(Peano axioms) a=b、a:二l;二(a二o)，(a二b浅a二c)、方二:c a=b、口二b .a十O=“，a十万二(a+b)’， a心二0，a.万二(a·b)十么及归纳公理模式 A(0)成vx(A(x)。A(x‘))。A(x)，其中A是任意公式，称为归纳公式(induCtion formula). 形式算术适合于推出初等数论中许多定理.到目前(1980)为止，还没有迹象表明存在某个不依赖于分析便可证明的重要数论定理在形式算术中不可证明.为在形式算术中表示和证明这样的定理，必须考虑形式算术的表示潜力，特别重要的是许多数论函数在形式算术中的可表示性.特别地，关于原始(甚至部分)递归函数(recursive仙1Ct泊ns)的命题也能用形式算术语言来表示这样，有可能证明表示部分递归函数重要性质的一些公式，特别是它们的定义方程.因此方程f(x’)二g(x，f伙》由下列公式表示 Va Vb Ve(F(xa)浅F(x，b)浅G(x，b，‘)、a“c)、其中，F，G分别是表示函数.f，叮的图形的公式.在形式算术语言中也能表示关于有限集的命题.此外，古典形式算术等价于一不带无限公理的Zermelo一Fraenkel公理集合论(axiomatie set theory飞:在这些系统中，任何一个系统的模型可以在另一系统中构造出来. 形式算术系统的推导能力由序熬(ordinai)￡0(方程。‘二。的最小解)来刻画:在形式算术中可以推出超限归纳法(transfinite induction)的模式直到任意序数:<:。，但不能推出到达￡。的归纳模式.形式算术系统的可呼谬归哟攀(Provably一!’ecut’sive fun以io。)类(即部分递归函数类，其一般递归性可由形式算术来确立)等同于序数<。。的序数递归函数类.这就有可能在某些方面扩展形式算术，例如，可以考虑带有表示所有本原递归函数的符号以及相应的附加公设的形式算术.形式算术满足两个G曰e】不完全性定理(G叱e}in~Pleteness theorem)的条件.特别地，存在多变元的多项式尸，Q，使得尽管丫X(p(幻)笋C(」均表示一个真命题—形式算术系统的相容性，但是这个公式不可证明.己经构造了一个独立于形式算术的(Ramsey型的)组合定理(【6〕). 在研究系统的结构(特别是相容性问题)时，形式算术的表述不含量词，但带有比nert的。符号.这个系统的公式是不带量词的，但允许用形如。、A(x)的项(如果*存在，则产生某个x满足条件A;否则为0).。系统的公设是:命题演算的公设，等号规则，自由数值变元的代换规则以及函数，=·，‘，pd(前驱)的公设，以及下面的￡公理: A(a)一A(￡二A(x》;魂(a)一气A(习祷a· 一:A(‘弓，A(x)丫~￡、通(x)=().量词可由下列公式导出; 日义A(x)#A(乓A(x));丫xA#二日x一1通.归约公理也是可推导的. 含自由变量的形式算术公式可定义数论谓词，不含自由变元的公式(闭公式(d伪ed formulas))表示命题.关于自然数的k元谓词少称为算术的(arithmet]c)，如果存在算术公式尸(、1，…，x*)使得对任何自然数n，，一”*，关系式 P(n1，…人)。<山，二nk>任少成立.这就由相应公式的前束范式的前束词的类型确定了算术谓词的一个分类.类艺。(类n，)是由形如 Q lxl…Q。凡叭;，，.，*。

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