【周祯祥】从动态命题逻辑PDL到动态道义逻辑DDL

 

一、动态命题逻辑的来源和基本构想

动态逻辑DL（dynamic logic）是关于行动和程序推理的形式系统。

DL可以描述为三个经典逻辑的合成：一是一阶谓词逻辑，二是模态逻辑，三是正则事件(regular event)的代数。DL区分于经典逻辑的地方是其真值的特性：经典逻辑的真值是静态的，一公式φ的真值由其结构中自有变元的取值所决定，公式φ导致的真值和赋值被看作为是不可改变的；相关于这些公式的任何其他值或者真值都无形式主义之说。[1]

而动态逻辑在这点上正好相反，在DL中，有清晰的被称作程序的语形结构，这些程序的作用就是改变变元的值，由此进而改变公式的值。例如，程序x：=x+1在自然数论域内改变了公式“x是奇数”的真值。

这些改变在经典谓词逻辑中，是在元逻辑的层次上产生。例如，在塔尔斯基对公式真值的定义中，如果u：﹛x，y，…﹜→N是变元在自然数N上的赋值，那么公式 就被定义为在赋值u下真，当且仅当存在一个 使得公式 在赋值u[x/α]下是真的，其中u[x/α]和u处处一致，除x之外，在x处公式取值α。这个定义涉及到一个元逻辑的运算，该运算对所有可能值 从u产生了u[x/α]。这个运算在程序x：=？形式的DL中变得日渐清晰，这些程序称作非判定性的或者称万用指派（wildcard）。这是一个相当不方便的程序，因为它不是很有效；然而，作为一个描述性的工具是相当有用的。获得y的平方根，一个更有效的方式，如果该方式存在的话，它就是程序：

（1）       x：=0；当（while） ＜y做（do）x：=x+1。

在DL中，这些程序是在公式面值之上的第一类对象，这些程序汇集了一组运算子以原子程序为基础归纳地形成复合程序。为了讨论一个在公式φ真值上的程序α的处理结果，DL使用了一个模态构造[α] φ。它的直观陈述是：处理起源于当前状态的α，并且暂停（halt）于满足公式φ的状态这是可能的。也有双向的模态构造[α] φ，它的直观陈述则是：如果α暂停在当前状态开始的时候，那么，它也会暂停在满足公式φ的状态之中。

一个实际的例子是，一阶公式 等价于DL公式<x：=？> 。为了用例子来有效说明量词，我们可以用while程序代替在方括号<>中的非决定性指派，范围在自然数N上，这两个公式是等价的。

除了对经典逻辑，计算理论和程序的严重依赖之外，DL在1960年代的后期在Thiele1966，和Engeler1967的著作中有最早的体现。这两位学者是第一个发展公式化理念并在一个抽象的设置中用形式系统处理程序性质的人。对程序证明的研究随后就蓬勃发展，出现了许多研究成果，其中著名的有Floyd1967的论文，Hoare1969的论文，Manna1974的论文，Salwicki1970的论文。第一个类似于今天DL的系统是由Salwicki1970论文中弄出来的，它受Engeler的启发而成。该系统被称作算法逻辑。一个类似的系统称作一元程序逻辑，这由Constable在1977年做成。真正的动态逻辑DL强调程序/断定的模态性质，这种DL由Pratt在1970年引进。

动态逻辑也被看作和行动（action）相关的一种逻辑，它一般讨论的是行动和过程的结构。1987年在斯坦福出版的教科书《时间和计算的逻辑》中，Rob Goldblatt对这一逻辑有详细的讨论。2000年，David Harel等人在剑桥MIT出版社出版《动态逻辑》的教科书，动态逻辑更广为人知。

带有符号[a], <b>的多模态语言可以看作是描述行动结果的一种逻辑，这种逻辑依赖于我们对互为影响的行动所具有的原初直觉。一个互为影响的行动系列可以用图表建立一个表示其相互关系的模型。箭头表示行动之间影响的方向，圆圈所示节点则可以表示某个行动所在的状态。如图所示：

在这个图形中，四个小圆圈指示了行动所在的状态，黑圆圈所在左边状态位置为西W，右边状态位置为东E，上边状态位置为北N，下边状态位置为南S。其中有些圆圈可能是起点状态，例如W边黑色节点；而有一些既是起点状态，又是终点状态，例如N边圆圈和箭头朝内的c行动所在的圆圈；有一些则是终点状态，例如S边圆圈。图中有3个行动a、b、c，显然，行动c是自反的，它不改变状态，由此可以把c行动看作是决定论的；N边状态是终端，没有从这个状态开始的行动。行动a和行动b可以互为取消影响；行动a和行动b的联合行动可以从W到S给出一个传递；也可以是从W到N的行动a，再由从N到S的行动B给出一个连续行动的传递。这样一个行动传递的过程实际上和一个计算机程序的传递过程是非常类似的。[2]

 

二、关于程序的推理

什么叫程序：一个程序就是某种形式语言表达的一种书写的方法。一个形式语言中所要处理的对象是：从给定输出的数据，计算出所要输出的数据。程序就表现为从数据输入到数据输出的计算方法。例如：两个整数的最大公约数gcd算法，可以编成一个程序，该程序实施的算法称作欧几里德算法。以变元x，y代表任意整数，取整数中的任意两个为输入。在变元x：中输出其最大公约数gcd。

当y≠0做

开始

z：=x mod y

x：=y；

y：=z

结束end

表达式x mod y的值是：当x被y用普通整数除法相除的时候，所获得的非负数的剩余部分。

程序通常使用变元去容纳输入和输出值以及中间结果。每一变元可假设来自一特指计算范围的值。计算范围是一个结构，它由数据值的集合构成，包括某些有区别的常元，基本的运算子以及测试（test），这里的测试是指可以操作在那些值上的测试，像在经典的一阶逻辑中的判定一样。在上述陈述中，x，y，z的论域都是在整数Z中，还包括基本运算，例如带余数的整数除法，还包括≠测试。如果把程序算法和数学中的变元通常用法相比较，程序中变元通常假定为在计算过程中的不同的值。无论什么时候一个指派x：=t，用其左边的x来进行操作，变元x的值都可以相应改变，

对程序的逻辑理解还需要我们继续来对状态（state）予以描述。我们在前面把一个行动放在某一个状态之中，在计算机程序中，对状态的理解类似于对行动状态的理解，赋值相当于某个行动。状态可以看作是一个函数，借助于赋值的行动，我们给每一个程序中的变元指派一个值。变元x的值必须属于和x相关的定义域。状态相当于我们在逻辑赋值时的时空背景，最容易设想的状态是时间状态。在程序处理数据的期间，时间序列中的任意一个瞬间，程序被认为是处在某个状态之中，由所有其变元的瞬间值所判定。如果一个指派陈述被处理，例如x：=2，那么该状态就改变到新的状态，也就是一个新的时间瞬间。在这一状态中，x的新值是2，所有其他变元的值仍和以前是一样的。

程序可以看作是在状态间的传输。给定初始状态（输入），程序将经历一系列中间状态，也许实际上在最后状态（输出）停止。状态序列被称为一个轨迹（trace），这样的状态序列发生在程序α处理的过程中，而程序α源出于一特指的输入状态。

 

三、PDL的语言

如同命题逻辑是所有逻辑的基础一样，DL的基础是PDL(Proposition Dynamic Logic)，DL是模态逻辑的一个重要分支，动态命题逻辑PDL当然也属于模态逻辑，它是涉及一元模态的逻辑；PDL的语言可以作以下简略描述：

这个语言有一般模态命题演算的基本词汇。

一个有限可能模态diamonds即◇，也就是可能模态的汇集，在PDL中该模态用<π>表示，其中，π是一个非决定论的程序。

一个断定公式<π>φ的含义可以解释为：从当下状态对π的某种终端处理导致了一个状态，在该状态中，保留了信息φ。

一个断定公式[π]φ则陈述了：从当下状态对π的每一种终端处理导致了一个状态，在该状态中，保留了信息φ。

PDL实际上没有什么新的东西，但有某种简洁的观念保证了PDL是具有高度的表达功能，可以使得那些程序的归纳结构在PDL的语形学中清晰地表达。

复杂的程序建构在基本的程序之外，这些基本程序使用了程序设计制造者的一些节目单。使用反映这一结构的可能模态算子，我们就获得了一个有力的和柔性的语言。

PDL的核心语言可以做如下理解。

假定我们已经固定了基本程序a，b，c的某些集合，则我们的基本模态就可以表述为<a>，<b>，<c>…。接着，我们允许去定义复杂的程序π，在这个基础上的模态运算子<π>就可以定义如下：

定义（选择）：

如果π₁，π₂，是程序，则π₁∪π₂，也是程序；

程序π₁∪π₂，（非决定论的）或者处理π₁，或者处理π₂。

定义（合成）：

如果π₁，π₂是程序，则π₁是程序，π₂也是程序；

这个程序先处理π₁，然后再处理π₂，；

定义（重复）：

如果π₁是程序，则π^*也是程序；

<π₁>,<π₂>这样一个程序，对程序π处理了有限次数，也可以是0。

由以上定义可得模态算子的复合定义

如果<π₁>,<π₂>是模态算子，则<π₁∪π₂>，<π₁,π₂>，<π^*₁>也是模态算子；

该符号可以直接来描述程序处理的性质。

可以用一个程序描述实例来说明PDL的语言用法。

<π^*>φ ↔φ∨<π；π^*>φ;

这个公式所表明的是，一个含有信息φ的状态可以通过对π进行有限次地处理而获得，当且仅当，或者是我们已经在当前状态中获得了信息φ，或者是，我们可以对π作若干次处理，在对π有限多次重复处理之后，我们可以找到一个状态，在这个状态中含有信息φ。

如果我们把程序建构的样式局限在以上三个：选择，合成和重复，我们所处理的逻辑就是称作正则的PDL，也是所谓Kleene的规则程序分析中的程序构建，但还有更宽广的程序构建，例如以下两个constructors：

定义（交）intersection：

如果π₁，π₂，是程序，则π₁∩π₂，也是程序；

程序π₁∩π₂，的意义是，既处理π₁，也处理π₂，用平行处理的方式。

更详细的解释可以是，如果我们在当前状态既处理π₁，也处理π₂，则至少存在一个状态被两个程序可达，而且这两个程序都含有信息φ；这是对多样性目的的一个自然的程序构建。

定义（测试）test：

如果φ是一个公式，那么φ？就是一个程序；

这个程序测试公式φ是否成立，如果它成立，就继续，如果不成立，就失效fail。

该test程序构建有其特殊的语形学：它允许我们把一个公式当作模态。直观地说，如果当前状态满足公式φ，这个模态就通达到当前的状态。

 

四、动态道义逻辑DDL（dynamic deontic logic）：PDL的运用和扩展

在2001年出版的哲学逻辑手册第二版中，有一段关于模态逻辑和计算机科学关系的描述。以该手册作者的观点看，今天，逻辑学很有可能在计算机科学中扮演十分重要的角色，并且，逻辑很有可能在这一重要的应用领域中获得新的发展从而促成逻辑科学的进化。今天，逻辑学和计算机科学的关系可以非常类似地理解为数学应用于物理学和工程学的关系。应用数学通过作为一个工具的使用而实现了数学的进化，逻辑也将在和计算机科学的结合中实现自己的进化。[3]

计算机科学中的动态逻辑，源出于对计算机程序的行动予以形式化，把它作为模态逻辑的一个分支，既是因为它有模态逻辑的基本特性，同时，它也为道义逻辑的发展提供了某种框架。促成状态变化的程序指令和行动的类比，使得动态逻辑用于道义逻辑有了可能。因此，这种动态逻辑一直被一些道义逻辑学家用来刻画基于道义逻辑的行动、断定等概念。[4]康格尔-安德森把应该是的道义逻辑归约到真势模态逻辑，而梅耶meyer则把应该做的道义逻辑归约到动态逻辑，这种归约的结果产生所谓动态道义逻辑DDL。动态道义逻辑DDL由梅耶等人发展起来，梅耶也把DDL看作是一种有些类似安德森类型的模态逻辑。

DDL的基础是命题动态逻辑的框架。道义运算子归约到动态运算子，即安德森曾给出的触犯原子V(violation)，这个算子的含义是：一个行动产生了对于某个道义强制规则的触犯，也就是，一个被禁止行动的实施导致了一个坏事态（bad state of affairs）.一坏事态可以产生某个制裁sanction，一种由过失行动而对制裁或者麻烦应负的责任liability。到底对坏事态的结果应该负有什么样的责任，则依赖于人们所坚持的哲学。一般对触犯常元V的解释是：在违反道德法律规范下的行动，就是一种触犯的情景.。

 

五、基于行动的动态道义逻辑DDL

在PDL中，带有符号[a], <b>的多模态语言可以看作是描述行动结果的一种逻辑，这种逻辑依赖于我们对互为影响的行动所具有的原初直觉，这种逻辑就是动态逻辑。动态逻辑中的模态算子符号[a], <b>可以稍作限定之后就运用到DDL中，道义逻辑由此可以作为动态逻辑的一个变体来看待。对道义逻辑的限定主要是行动和断定的区分，只要我们对行动和断定做出了严格的区分，把道义逻辑归约到行动逻辑就有了可能。

依据梅耶的说法，行动和断定命题的区分在于，一个行动它可以改变当前的状态，但是一个断定命题则不具有改变状态的功能。断定总是对命题的断定，断定没有给出行动或者予以操作的功能。在DDL中，如果我们把公式Φ看作是一个断定陈述，这个陈述说的是：行动α是应该的，我们继续陈述命题Φ是应该的，把它标示为OΦ，实际上是OOΦ，这样一种陈述在DDL中是没有意义的，它不是该系统中的一个合式公式。[5]

对应于计算机程序的动态逻辑，动态道义逻辑把断定（assertion）和行动严格地区分开来，同时在DDL中增加了一个时间缝隙（time-lag）概念。一个道义逻辑的规范命题：β是禁止的，它可以表示为：F（β）,其中，F代表禁止（forbidden）。我们对规范命题的这一理解，由断定和行动的区分，就可以归约到某种动态表达式: F（β）=[β]V。其中[β]V所表达的含义是，如果我们实施了或者做了一个被禁止的行动，那就是触犯了规范，进一步就是接受惩罚。F（β）由此也就成了被禁止的行动，而不是作为一个断定而言的。这时候，β不是一个被规范的命题，而是一个被规范的行动。

由对禁止的理解可以很容易地过渡到道义模态允许P和应该O的表述：

P（β）=〈β〉┐V；

O（β）=[β]┐V；

把β看作是行动，传统道义逻辑中的否定词用到行动β上，就具有行动的不实施的意义，可以把这种否定的行动用加上横线的符号 来表示，这个符号的意义就是并非实施了行动β。

一个简化了的DDL是对行动范畴的进一步限定，如果我们不考虑行动的系列，仅以原子行动作为我们讨论DDL行动的起点，则DDL的建构可以简化为行动的语形学和行动表达式的语义学。在这个基础上，我们就可以继续地探讨被我们分离开的行动表达式和道义断定表达式，从而构建在DDL框架中一个道义断定的语言Ass。在行动表达式的语义学中，行动和世界（场所，环境）紧密相联系，这种语义学可以参照模态逻辑的可能世界语义学观念来理解。

DDL的断定语言Ass的语义学则可以依据行动表达式的语义学构建，把传统道义逻辑中相应符号和公式归约到动态逻辑。由这两者的构建，形成一个DDL的模型。这个构建过程的简略细节可参看〈为法律规则形式化而扩展的道义逻辑〉一书，该书既探讨了道义逻辑在SDL（Standard Deontic logic）方向上，道义逻辑的一些新的视野，还专辟第三章论述道义逻辑在动态逻辑方向上的发展。[6]

DDL是计算机的程序逻辑-动态逻辑在道义逻辑领域中的一个有益尝试，由于规范本质上是和行动个体紧密相联系的，而应该做（ought to do）的语句又总是表现为法律规则，所以DDL作为道义逻辑的一个扩展，在法律的表达和解释方面提供了一个新的视角。此外，DDL的出现，对于澄清行动和道义断定之间的区别和联系，对于消解在传统道义逻辑中常常出现的背离直观的道义悖论都具有其他逻辑构建所不能替代的作用。

 

 

（原载《哲学动态》2006年第2期。录入编辑：wxl）