补充资料：形式系统

形式系统
fonnal system

　　形式系统[匆翻旧.邓加n;中叩Ma“a，c一c，Ma]，簿绎系统(deductj姆s声t巴n) 由构成表示式的规则以及在这个演算中构成推导(见逻辑推导(山d份血n，lo乡Cal))的规则给出的数理逻辑中的一种演算(。目c』‘).形式系统的表示式被看成是一些符号的纯粹形式的组合，而推导规则决定什么情况下形式表示式A能由另外一些表示式B，，…，凡演绎出来.当”一0时，A就称为兮浮(~m).推导是由形式表示式依据推导规则给出的一个序列，或树形图表.如果一个推导树形的顶点上只有公理，则位于这个推导末尾的一个形式表示式称为在这个形式系统中可推导的(山巧姐ble). 许多感兴趣的形式系统，其语言和推导都满足能行性(effectj、en已粥)要求.这就是说必须要有一个能行的程序来判定任意一个符号序列是否是这个形式系统的表示式.推导概念也必须满足同样的要求.但一般说来，在一个能行形式系统中，可推演的表示式这个概念不是能行的. 形式系统这个概念是数理逻辑中最核心的概念之一，它既适用于数理逻辑本身，也适用于数学的有关领域的需要. 最重要的一类形式系统是形式化某个有意义的数学分支的形式一阶理论(见【4」).历史上，这一类形式系统的出现与D.HUbert为给出数学的基础而作的计划有关(见形式主义(fom创ism)). 为研究形式系统而在数理逻辑中发展起来的概念和方法已经在数学的各个分支，例如群论和范畴论中得到应用. 亦见形式数学分析(fon们以In迢therr以ti司anal那is).
　　

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