补充资料：逐步语义系统

逐步语义系统
stepwise semandc system

逐步语义系统!ste沙isese兹.涌c卿st助;cTylle。，aT.ceMa.”气ecK，c“cTeMaj 一个由Markov在互2」夕f31中提出的构造性语义学的变种.在这个系统的构造中对一个语义学问题—蕴涵(川IPlica力on)的构造性解释给予了特别的重视.传统的直觉主义对论断(AOB)的解释是，(A OB)表示结构p的可实现性，使得如果q是任意一个断言A的结构，那么p和q一起就可能找到一个断言B的结构.这个非形式的解释从很多方面考虑并不能引导到一个精确的定义，Markov的想法是，蕴涵(A“B)可以被考虑成为用含有无限归纳法原则的理论(一个半形式化的理论(s。的l一化rznal theory))作为手段形成由前提A推导B的论断.因此，问题中的半形式化的理论以及公式A和B的语义可以在构造的早期阶段就得到解释.作为结果一个逐步语义系统产生了，其中作为下一步的公式的意义是用前一步的对象来定义的. Markov构造了两个互相等价的逐步语义系统的变种—“长塔”t2]和“短塔”汇3〕.下面简单地在谓词演算(predicate calculus)的传统记号以及形式算术(forl花d颐如拙tic)的语言中对短塔作出解释(Mar-kov自己用了不带括号的公式记号).语言L。的初等公式采取(t二;)或(t笋r)的形式，其中t，r为原始递归项(L。的项).采用逻辑运算合取(c onjunc-tion)八，析取(disjunction)V以及限定皿词(restri-cted quan山滋r)(丫x‘t)中，(日x簇r)毋，其中沪是L。中的一个公式，而t是L。中的一个项，其他L。的公式可以用通常方式构造出来.语言L。在存在一个由全体L。的式子中辨认出真的闭式子来的一般方法的意义之下是可判定的.L。的公式的语义是由对于公式的结构作归纳法来定义的.每一个L。的公式都等价于一个没有量词的公式. 乙，的公式是由L。的公式利用任意数量的V，八以及存在量词构造出来的.语言L，是不可判定的，但是可以构造一个演算C，在它里面恰好真的闭式子可以推演出来.L:的公式是由L、的公式通过一次使用运算。和任意多次使用运算八和量词丫归纳地构造出来的.因此L:的公式采取如下形式的一种:l)L:的公式;2)(价八沙)，其中尹，价是LZ的公式;3):。刀，其中:，刀是Ll的公式;4)丫x:，其中甲是LZ的公式.蕴涵(仪“川解释如下:(，“刀)表示一个一般的方法出现，它对于语言字母表中的任意字Q，或者能确立Q不是二在C中的一个推演，或者能在C中给出刀的一个推演.一个半形式化的理论s:就这样地被构造出来，其中L:的闭式子可以被推导出来(对Ll而言S:的角色由C来扮演).L:的真公式是S:的公理.在通常的推演规则之间有带有无限多个前提条件的有效的。

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