动态逻辑的双重性：程序化与结构化

郝一江

（中国社会科学院哲学研究所，北京 100732）

现代逻辑学是信息时代的核心基础理论。王元元教授在其专著《计算机科学中的现代逻辑学》中指出：现代逻辑学与计算机科学是“天生的同盟军，分别作战在基础理论和实用技术两条战线”；“现代逻辑求助数学——符号化，现代逻辑追随数学——公理化，现代逻辑改造数学——形式化”[1]。简言之，现代逻辑学具有符号化、公理化、形式化这三个普遍性质。作为现代逻辑学的主要分支学科的动态逻辑，不但具有这三个普遍特征，而且还具有程序化特征和结构化特征。动态逻辑之所以具有程序化和结构化的双重性，其根本原因就是现代逻辑的数学化。

关于数学与逻辑的关系问题，布尔学派指出：“逻辑学是数学的一个分支”；弗雷格学派则坚称：“数学是逻辑学的一个分支”[2]；罗素认为：近代以来，“逻辑更数学化，数学更逻辑化”，“事实上二者也确实是一门学科”。[3]以上这些观点其实都从不同角度揭示了数学与逻辑的本质及其交互规定：数学的本质是逻辑，逻辑的本质是数学；这种共同而有区别的本质不但为数学史所验证，也为逻辑史乃至于哲学史所验证。因此，对逻辑的哲学思考，亦是对数学的哲学思考。

由于数学与逻辑交互规定，互相构成对方的本质，因此动态逻辑具有数学所具有的普遍特征，如：符号化、公理化、形式化。此外，数学已经进入了微积分、实变函数论、复变函数论的时代，泛函分析主导拓扑与抽象代数的时代，数学语言的本体论基础是实数系统和集合论，连续的直线已经完成了时间化和离散性重构，动态逻辑的语言也实现了离散化，这为动态逻辑的程序化和结构化打开了通道。

一、数学与逻辑的交互规定

在影响数学与逻辑交互规定、交互解释、交互表征的所有因素中，语言处于枢纽地位，发挥决定性作用，语言是数学与逻辑的基础框架，任何有意义的数学与逻辑表达式，都在语言之中按照语法规则构成，正是在这个意义上语法规则称为形成规则[4]9。数学与逻辑的语法构成推动了数学与逻辑的历史展开，语言的因素导致数学与逻辑互相构成对方的本质[5]15。

根据胡塞尔的《逻辑研究》，广义的逻辑除了命题层次的形式逻辑，还有对象层次的形式本体论。在这个宏大的历史视野中，集合论的创立及其对于数学的重构就有了超越数学史的哲学意义。几何研究的图形和代数研究的数都是名词命名的对象，而集合论研究的集合是命题表征的概念，它们属于完全不同类型的语法和意义范畴，名词不是表达意义的完整的语言单位，命题却是这样的语言单位，因此集合论在历史上第一次把存在纳入了意义的范畴，使存在从属于概念而成为概念的衍生样式[6]83。

存在与本质是概念的变化形态，因此它们成为概念的内部环节；概念不是事物不是对象，概念是语言的意义，因此存在与本质脱离了事物，被提升到语言的境界。意义获得了自身的存在和本质，既是对语言的提升又是对存在的充实，语言不但拥有了自己的意义与概念，而且拥有了自己的存在与本质[6]87。

集合论第一次让人们看清了这样的事实：无论数学还是逻辑都是一种语言现象，一种由语法的构成所体现出来的意义的建构，现代数学的宏伟大厦，乃至于整个科学大厦，都是建立在对符号及其语法构成的深刻而清澈的直觉的基础上，建立在对符号的语法构成所引发的推理链条的深刻而清澈的直觉的基础上[4]14。

由于数学是科学的先行筹划与先行规定，因此科学也是镶嵌在语言及其语法之中的，从而成为历史、文化和意识形态的一个片段。在这种意义上我们可以回应罗素，数学乃至于所有科学，其本质和逻辑一样与希腊文有关，都是建立在对希腊文的语法及其产生的推理链条的理性直觉之上，正是通过对语言和语法及其逻辑的直觉，数学和科学通过意义的道路切入了存在问题，进入了时间和历史之中，因而打开了文化和意识形态的视野[5]20。

在逻辑实证主义奉为圭臬的《逻辑哲学论》中，维特根斯坦提出了可以显示不可言说的思想，为逻辑的形式化划出了一条界限。接下来哥德尔以其著名的不完全性定理验证了维特根斯坦的直觉思想，分析哲学及其数理逻辑在命题层次对数学所做的形式化表征与刻画是不完全的，形式化不但不能消除直觉，而且必须依靠直觉以获得其意义与解释。这就是《存在与时间》第33节的主题和标题：“命题——解释的衍生样式”，谓词的解释与构成功能先于谓词的表述与判断功能，谓词对于约束变元的建构使得命题成为可能，谓词对于变元的建构形成了结构，在本体论上结构不是事物而是事实，因此维特根斯坦认为，世界是事实的总和，不是事物的总和。维特根斯坦的事实的本体论为海德格尔的此在分析所拓展，《存在与时间》第70节“此在式空间性的时间性”进一步明确了：所谓事实的本体论是植根于此在的时间性的空间结构，支撑这种空间建构的语法过程是谓词的解释行为，这与支撑命题构成的图象行为属于迥然不同的语法类型，正是在这种意义上，根据在其背后作为支撑的不同语法类型，维特根斯坦划分了命题与事实：命题是事实的图象[6]83-87。

20世纪60年代，奎因发现，就在符号逻辑的形式化语言中，存在通向本体论及其语言和语法建构的逻辑通道，这就是其著名的论题：存在就是作为约束变元的值。这样整个数理逻辑的理论成就，经过数学哲学的范式转换，都可以进行数学语言的存在建构，就在这种从表述到解释语法的转换中，数学的结构特征自然地呈现出来。

二、动态逻辑的程序化特征

程序不仅是计算机能够识别和执行的指令，而且也是表征输入/输出数据关系的形式语言。动态逻辑是多个程序逻辑的总称，能够对程序的输入/输出行为进行形式化表示和推理的多模态逻辑[7]133。动态逻辑的两个核心系统是命题动态逻辑和量化动态逻辑[8]。动态逻辑及其扩展逻辑可以对Agent（智能体）行为决策、行为规划和行为学习等进行表征和推理。

动态逻辑是关于程序的多模态逻辑，是由多个系统组成的丰富家族，是用每个程序的一个给定模态词对经典逻辑加以扩展而得到的[7]xi，因此动态逻辑是程序化的多模态逻辑，具有明显的程序化特征。例如：

在命题动态逻辑中，用程序设计语言的程序来填充模态算子[]（即box算子）。[a]φ表示：执行程序a并在满足状态φ时停机是必然的；[a]φ也可理解为：在每次执行程序a后，公式φ为真。除了原子程序可以填充box算子外，由选择算子∪、合成算子；测试算子?和迭代算子*这四类程序复合算子构造的复杂程序也可以填充box算子[7]164-170。[a∪β]φ表示：在每次不确定地执行程序a或β之后，公式φ为真。[a;β]φ表示：在每次“先执行程序a，然后执行程序β”之后，公式φ为真。[a]*多次重复执行程序a之后，公式φ为真。

带有正则程序（regular program）的命题动态逻辑的三个初始算子“；∪和*”都是正则表达式，程序是在原子程序和测试上的正则表达式。其命题和程序是由原子命题、原子程序，通过命题否定算子（ 00）、命题蕴涵算子（→）和以上四个程序复合算子递归得到的；而且利用这6个算子可以得到所有的while程序。其程序和命题的定义也可以相互递归，具体地说：如果φ和ψ是命题，a和β是程序，那么φ→ψ、 00和[a]φ是命题，而a∪β、α;β、φ？和a*都是程序[7]169-170。

由此可见，动态逻辑使用了各种程序算子，它的一些逻辑公式本身就是面向对象的程序语言，因而动态逻辑具有程序化特征。此外，动态逻辑的一些变种也具有程序化特征。例如带有程序量词的命题动态逻辑[9]、带有互模拟程序的命题动态逻辑[10]、带有Petri网的命题动态逻辑[11]、带有有穷多个量词的命题动态逻辑[12]、带有存储、恢复和并行合成算子的命题动态逻辑[13]、能够对Agent能力进行推理的类型命题动态逻辑[14]、能够对Agent规划修订进行推理的扩展命题动态逻辑[15]等都具有程序化特征。

三、动态逻辑的结构化特征

由于集合论对于现代数学的无所不在的广泛影响，及其对数学研究方式和数学思想观念的深刻变革，结构主义从20世纪以来逐渐占据了基础数学和数学哲学的主导地位，并且产生了溢出效应，从而使得“从结构的角度观察逻辑的特征”成为可能：从语法上看，形式化的逻辑系统是不同符号按照各种关系组成的结构，这种结构可以通过元数学加以研究；从语义上看，所有逻辑命题都是通过定义在集合之上的数学结构加以解释；从语法和语义的关系来看，逻辑系统的元逻辑性质由这两种结构的关系决定，一个逻辑系统是可靠的，当其语法结构不表达其语义结构以外的信息；一个逻辑系统是完全的，当其语义结构的信息都由其语法结构表达出来。

动态逻辑是在集合论和模态逻辑的基础上发展起来的多个程序逻辑的总称。集合论不但是动态逻辑的基本语言，也是定义数学结构的前提和产生数学结构的基础与载体，因此，数学结构对于动态逻辑的渗透是全方位的，无论是在语法上还是在语义上，以及语法和语义的关系上。在语法上，动态逻辑的结构特征是非常明显的，动态逻辑中的诸多规则本身就是结构性规则。例如：能够对Agent能力进行推理的类型命题动态逻辑tPDL给出的Gentzen系统中的规则，分离规则、必然性规则、否定规则、导出规则、切割规则、交换规则、缩并规则、弱化规则、传递闭包规则、循环不变性规则等，都是结构性规则[14]。

在语法和语义的关系上，结构的作用体现在完全性和可靠性等元逻辑性质的证明上，当语法结构的表达力强于语义结构的表达力时，动态逻辑具备完全性而不具备可靠性，当语义结构的表达力强于语法结构的表达力时，动态逻辑具备可靠性而不具备完全性，当语法结构的表达力等于语义结构的表达力时，动态逻辑同时具备完全性和可靠性。例如，利用动态逻辑及其扩展对Agent的各种行为进行形式刻画或建模，其实质是形式化地描摹决定Agent的各种行为因素的内在结构。利用类型命题动态逻辑τPDL对Agent能力进行描述时，首先使用能力语句、先决条件-效果结构和向后可能算子对标准命题动态逻辑PDL进行扩展得到τPDL，通过建立有穷模型性质，利用标准的滤过技术，在扩展的Fisch⁃er-Ladner闭包映射的基础上，可以证明τPDL系统的可判定性，给出τPDL逻辑的证明系统，并可以研究其可靠性和完全性，并且可以把τPDL逻辑应用于网络服务组合[14]。上述一系列的证明步骤离不开对逻辑系统的构造，离不开对解释系统的数学结构的构造，离不开对系统的表达力与解释系统的结构的表达力的衡量，因为在元数学中，逻辑系统也是定义在有穷或者无穷集合上的数学结构，是在语法意义上的数学结构。

最能体现动态逻辑的结构化特征的还是语义方面的数学结构。在语义方面动态逻辑涉及到各种各样的结构[7]，如：克里普克结构、树状结构、Adian结构、表征结构、有穷结构、无穷结构，等等。这些都是定义在有穷或者无穷集合上的数学结构。具体而言：

（1）动态逻辑的语义源于模态逻辑的语义，动态逻辑的程序和命题都可以在克里普克框架结构上加以解释，而克里普克框架的具体结构及其包含的元数的个数都是由所涉及集合上定义的数学结构决定的。

（2）可以给出量化动态逻辑在算术结构上的解释性推理[7]308-311。事实上，任意动态逻辑的结构都可以通过添加适当的编码和解码功能对算术结构进行扩展而得到；而且每个自然数集上的结构都可以扩展成算术结构。

（3）动态逻辑表达力的强弱依赖于“该逻辑是在哪种结构中加以解释”。例如：当对所有结构进行统一解释时，一阶逻辑、量化动态逻辑、正则量化动态逻辑、带有富测试的量化动态逻辑形成了一个表达力越来越强的逻辑序列。但是在任意算术结构上，前三种逻辑的表达力是一样的，最后一种逻辑的表达力比前三种逻辑强[7]308-311。

（4）动态逻辑可以对有穷结构进行编码。例如，可以对“如线性序排列的一阶有穷词库S中的”有穷结构S进行编码，进而可以研究结构S1与结构S2是否同构。研究表明：富词库与穷词库的主要区别在于：富词库允许具有“给定有穷基数而且具有指数多个两两不同构的”结构，而穷词库仅仅允许“给定有穷基数而且具有多项式个两两不同构的”结构[7]319-320。事实上，同构概念本身就是比较作为论域的集合上的数学结构之间的关系。

（5）动态逻辑中的一些定义都是在某种结构中加以定义的。例如：一个程序α可以在结构S中展开（unwind），当且仅当，存在 m∊N（N是自然数集）且存在有穷计算序列 σ1,...,σm∊CS(α)，使得 f(α)=f(σ1)∪…∪f(σm)，其中CS(α)是可枚举的有穷计算序列集，f是意义函数。这一定义就是在结构这一概念上加以定义[7]344。

（6）动态逻辑中的一些命题需要借助结构这一概念才能够加以阐述的。例如，动态逻辑的如下命题：“如果S是一个不带有真子结构的无穷结构，则NEXT0在S中不展开”[7]344-347。阐释这一命题需要借助真子结构和无穷结构这两个概念。

（7）动态逻辑中的诸多归纳证明，都是施归纳于解释动态逻辑的数学结构。例如：能够对Agent能力进行推理的类型命题动态逻辑关于滤过引理的证明，同时施归纳于公式ψ或类型A以及良基FL-子公式关系的结构[14]。由此可见，在语义方面，动态逻辑不但涉及各种各样的数学结构，而且这些数学结构所的作用也是多种多样的。

四、结束语

对于动态逻辑来说，无论是其与现代逻辑各分支共有的普遍特征，如：符号化、公理化、形式化，还是其独有特征（即程序化、结构化），这些特征的根源都在于：数学与逻辑的交互规定，数学与逻辑互相构成对方的本质，以及数学内部代数与几何的根本矛盾，这种矛盾所导致的数学的历史阶段和体系结构——几何、代数、微积分。微积分统一了代数与几何，作为微积分基础的实数系统和集合论统一了时间和空间，实现了空间的时间化和时间的空间化，这样就开启了通过离散表征连续的人工智能时代，以集合论为语言、具有程序化和结构化特征的动态逻辑成为这个时代典型的标记。