理想信息流逻辑的树图系统，本文主要内容关键词为：信息流论文,逻辑论文,理想论文,系统论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
中图分类号：B813 文献标识码：A 文章编号：1001-5019(2011)01-0059-08
一、理想信息流逻辑的理论背景
现代信息流思想起源于申侬(C.E.Shannon)的通信理论。上世纪80年代初哲学家德雷斯克(F.I.Dretske)从语义角度对通信理论中的信息流思想进行发展，提出一个信息内容理论。受德雷斯克思想的影响，逻辑学家巴维斯(J.Barwise)和语言哲学家佩利(J.Perry)在上世纪80年代提出情景理论，之后巴维斯又在情景理论基础上提出信息通道理论。情景理论和信息通道理论将现代信息流研究推向一个新的高度。信息通道理论将情景之间的联系视为信息通道，认为信息通道与情景类之间的制约关系之间存在分类关系，强调信息流不仅涉及情景类之间的联系而且涉及情景之间的联系。根据信息流的直觉原则，信息通道理论将信息流定义为：假设s和t是任意两个情景，A和B是任意两个情景类，如果用s：A表示s属于A，用A
B表示A和B之间的制约关系，用
表示c是从情景s到情景t的信息通道，那么s：A传递信息t：B当且仅当存在一个信息通道c使得
。信息通道之间的不同复合运算是信息通道理论的重要组成部分。
根据以上信息通道理论，巴维斯与逻辑学家盖贝(D.Gabbay)和哈特纳斯(C.Hartonas)于1995年合作撰文构造出一个信息流逻辑（简称BGH）②。他们的研究有两个基本视角：其一，制约关系使信息流动，这是情景理论中信息流思想的核心；其二，信息通道是个体之间的联系，信息通道与制约关系之间存在类属关系③。BGH的形式语言包括表征情景类之间、情景类与信息通道类之间和信息通道类之间不同信息流运算的四个信息流联结词→、←、↓和o；根据信息通道与情景是否同类，其形式语言可以是单体的也可以是双体的；BGH的形式系统是包括恒等公理、删减规则和联结词规则的甘岑后承系统，这些系统被证明具有可靠性和完全性。BGH表征理想信息流推理。
如果孤立地看BGH，它构造巧妙精致，称得上是成功的逻辑系统，虽然有些“另类”④。但如果从外部来看，BGH尚有一些不足或缺憾。首先，虽然BGH信息流逻辑的主要依据是巴维斯的信息通道理论，但它并没有涉及该公理理论所列举的五条直觉原则。另外，除序列复合之外，信息通道之间的其他复合运算在BGH信息流逻辑中并没得到体现。再者，信息通道理论将现代逻辑意义上的逻辑推理视为情景内信息流推理，信息流逻辑应能够解释逻辑推理，但BGH信息流逻辑对此亦无反映。针对BGH的不足或缺憾，本文将构造新的信息流逻辑来刻画理想信息流推理。语义上，我们将视信息通道与情景同类，对情景类与信息单位不作区分，用
表示情景与信息单位之间的支持关系。情景之间的信息流被如下定义：如果
。据此，我们可以说这三个情景之间存在信息流关系。信息流关系可以具有不同性质。根据信息流关系的不同性质，可以有不同类型的信息流推理。语形上，我们将设置一个信息单位语言，只保留BGH中的信息流算子→并引入否定、合取和析取等布尔算子，其中→被称为信息流蕴涵算子。我们将构造理想信息流逻辑的树图(tableau)系统，因为我们认为树图系统能够较好反映信息流逻辑语形为语义服务的特点。我们将根据信息流关系的不同性质设置不同推理规则表现理想信息流推理的不同情况。
二、理想信息流逻辑的
形式语言和语义解释
（一）理想信息流逻辑的形式语言
（二）理想信息流逻辑的语义框架和模型
理想信息流逻辑的基本语义框架是如下定义的信息框架。
须注意：具有自返性质的信息流关系有如下特殊情况：
u,s,t∈S(Rustu=s=t)；具有持续性质的信息流关系有类似特殊情况：s∈S(Rsss)。
我们还可以定义信息流关系的更为复杂的性质，如自返且对称且序列、序列且并列等。
定义4 令IF=＜S,R＞是任意信息框架，IF是自返或对称或持续或稠密或序列或并列信息框架，当且仅当，R具有相应性质。
根据信息流关系的复杂性质，我们可以有复杂信息框架。
不同的信息框架支持不同种类的信息流推理。
根据IF中R的不同性质，我们分别有自返信息模型、对称信息模型、持续信息模型、稠密信息模型、序列信息模型、并列信息模型。
（三）可满足关系和信息有效性
仿照巴维斯等人信息流逻辑研究中的做法，我们可以给出信息流后承的概念，然后据此定义信息有效性。
因为我们下面所构造信息流逻辑系统中的定理都是信息流后承，所以我们需要一个相对于信息流后承的有效性概念，并以此有效性来证明这些信息流逻辑形式系统的相关特征。
三、理想信息流逻辑的树图系统
树图证明的方法由波斯(E.W.Beth)和辛迪卡(J.Hintikka)在上世纪50年代首创，之后斯穆里安(R.M.Smullyan)和费廷(M.C.Fitting)对这种证明方法加以改进，普瑞斯特(C.Priest)采用树图证明的方法对各种非经典逻辑进行了系统描述。如今，树图证明的方法已成为现代逻辑研究中最为流行的证明方法之一。⑤我们选用这种方法是因为这种证明方法符合信息流逻辑研究的要求。在现代逻辑的主要证明方法中，树图证明的方法和由此构造的形式系统体现明显语义特征⑥，它使语形证明和语义解释在逻辑系统中都得到呈现，使语形证明贴近直觉⑦。树图证明的方法可以被视为一种寻找满足某些条件的模型的程序，一个树图的每个分枝都可以被视为是对一个模型的一个部分描述⑧。树图证明使逻辑系统的完全性的证明简单可行。
图1 信息流后承树图
一个信息流后承树图是如图1所示的一种构造。其中的黑点称为结点(nodes)。每个结点处都存在一个有穷序列，该序列中的元素分为两种：一种是由一个信息元表达式和一个数字组成的对元素，形如(σ,i)；另一种元素形如irjk，其中除r之外的小写英文字母都表示一个自然数。最上端的结点称为树根，最下端的结点称为树叶，从树根到一个树叶的路径称为一个分枝。一个树图有几个树叶，它就有几个分枝。箭头的方向表示树图生长的方向。
理想信息流逻辑的内定理都是以信息流后承的形式呈现。通过构造一个信息流后承的相关树图，我们可以判断它在一个信息流逻辑系统中是否成立。为信息流后承构造树图的过程是一个从树根出发依据一组树图规则逐渐长出新枝的过程。理想信息流逻辑的树图规则包括一组联结词规则和表征不同信息流关系的一组R规则。
联结词规则：
这些规则中箭头之上的成分表示该推理的前提，即在使用该规则之时树图中已经出现的成分；箭头之下的成分表示该推理的结论，即通过对树图中已经出现的一些成分使用该规则得到的新枝。
联结词规则中的→则和┐→规则表征信息流推理的可靠性条件，而每个R规则表征一类信息流推理：r规则表征自返信息流推理，s规则表征对称信息流推理，e规则表征持续信息流推理，d规则表征稠密信息流推理，t表征序列信息流推理，p规则表征并列信息流推理。
定义10 信息元语言
信息元表达式形成规则和以上联结词规则构成信息流逻辑的极小树图系统，记作IS。根据以上规则为某信息流后承构造的树图称为该信息流后承的IS树图。通过在IS的基础上增加一个或多个R规则，我们可以得到IS的不同扩张。
下面来解释如何利用这些树图规则为信息流后承构造树图。
定义11 对信息流后承树图中的一个分枝使用一个树图规则得到的一个新枝称为该分枝的一个扩展。如果对一个分枝使用一个树图规则得到一个新枝，则该分枝有一个扩展；如果对一个分枝使用一个树图规则得到两个新枝，则该分枝有两个扩展。
信息流后承树图的构造过程是从树根到树叶的一个生长过程。为了给信息流后承Γ├σ构造一个树图，我们应该首先确定树图的树根。置于树根处的是一个有穷序列，称为初始序列，该序列包括由Γ中各信息元表达式与某字母组成的对和由┐σ与某字母组成的对。通过不断使用以上树图规则，我们可以不断得到新枝，最后得到的结果就是该信息流后承的一个IS树图。
对于初始序列中信息元表达式与自然数之间组对，我们有如下规定：
这样的规定与定义9相一致。
定义12 一个分枝是完全的，当且仅当，每个能被使用的规则都被使用；否则它是不完全的。一个树图是完全的，当且仅当，它的每个分枝都是完全的；否则该树图是不完全的。
定义13 一个分枝是封闭的，当且仅当，有形如(σ,i)和(┐σ,i)的两个对在该分枝中出现；否则它是开放的。在一个分枝的数叶下添加标记×表示该分枝是一个封闭分枝。在构造树图过程中，对于封闭分枝，我们不再对之使用规则进行扩展。一个树图是封闭的，当且仅当，它的每个分枝都是封闭的；否则它是开放的。即，一个树图是开放的，当且仅当，存在一个开放分枝。
四、理想信息流逻辑的可靠性和完全性
以上构造的理想信息流逻辑树图系统具有可靠性和完全性的系统特征，下面我们只给出IS的可靠性和完全性的证明，不同IS扩张的可靠性和完全性的证明可据此完成。
（一）IS的可靠性特征及其证明
定理1（IS可靠性定理） 在信息流逻辑IS的树图系统中成立的每个信息流后承在任意信息模型IM中都是有效的。即，如果Γ├σ，那么Γσ。
IS可靠性定理的证明需要以下定义和引理。
定义15 令IM=＜S，R,V＞是任意信息模型，b为一个树图的任意分枝。IM满足b，当且仅当，存在一个从自然数集合N到S的一个映射f，使得：
(1)对于分枝b的每个结点上的对(σ,i)，存在f(i)∈S使得IM,f(i)σ；
(2)如果irjk在b中，那么，在IM中存在f(i),f(j),f(k)∈S使得Rf(i)f(j)f(k)。
我们说，f表明IM满足分枝b。
引理1（可靠性引理） 令b是一个树图的任意分枝，IM=＜S,R,V＞是任意信息模型，如果IM满足b并且对b使用一个树图规则，那么IM至少满足b生成的一个扩展b'。
证明：令f是表明IM满足分枝b的一个函项。我们需要逐个考察IS树图规则，这里仅考察其中三个规则，其他规则与此类似。
（二）反模型
为信息流后承Γ├σ在一个信息流逻辑树图系统IS'，中构造树图的过程，实际上是系统寻找使得初始序列中每个信息元表达式相对于某情景⑩成立的一个信息模型的一个过程。如果构造出来的IS'树图是一个封闭树图，则说明我们找不出这样的信息模型，即找不出既满足该后承前提中Γ中所有信息元表达式又满足┐σ的信息模型，亦即凡是满足Γ中各信息元表达式的信息模型必定满足σ。根据后承有效性的定义，这表明信息流后承Γ├σ在所有信息模型中信息有效。如果构造出来的IS'树图是开放树图，则表明我们可以找出这样一个既满足该后承前提中Γ中所有信息元表达式又满┐σ的信息模型，即该信息模型满足Γ中各信息元表达式但不满足σ。根据后承有效性的定义，这表明信息流后承Γ├σ并非在该信息模型中有效。
我们可以用反模型方法来证明信息流逻辑系统的完全性特征。
（三）IS的完全性特征及其证明
定理2（IS完全性定理） 在所有信息模型中有效的信息流后承都是在信息流逻辑IS的树图系统中可推出的。即，如果Γσ。那么Γ├σ。
IS完全性定理的证明需要以下定义和引理。
定义18 令b是一个树图的一个开放分枝。b所引发的信息模型IM是任意信息模型IM=＜S，R,V＞使得
同理可证σ在b中出现的其他情况。证毕。
接下来我们来完成完全性定理的证明。
注释：
①J.Barwise,Constraints,Channels,and the Flow of Information.In P.Aczel,D.Israel,Y.Katagiri,S.Peters (eds.),Situation Theory and Its Applications,vol.3,Stanford:CSLI,1993,pp.3-28.
②J.Barwise,D.Gabbay,C.Hartonas,On the Logic of Information Flow,Bull of the IGPL,vol.3,no.1,1995,pp.7-49.
③J.Barwise,D.Gabbay,C.Hartonas,On the Logic of Information Flow,Bull of the IGPL,vol.3,no.1,1995,pp.7-49.
④张清宇：《逻辑哲学九章》，南京：江苏人民出版社，2004年，第347页。
⑤M.D'Agostino,D.Gabbay,R.Hahnle,et al,Handbook of Tableau Methods,Dordrecht:Kluwer Academic Publishers,1999,p.vii.
⑥张清宇指出，“这样的系统（指树图系统）在一定程度上已经引入真值（部分语义）”。《逻辑哲学九章》，第56页。
⑦M.D'Agostino,D.Gabbay,R.Hahnle,et al,Handbook of Tableau Methods,p.vii.
⑧M.D'Agostino,D.Gabbay,R.Hahnle,et al,Handbook of Tableau Methods,p.1.
⑨如果Γ中只有一个信息元表达式ψ，那么i=j。
⑩如果初始序列中有两个以上的对，那么它们中的每个信息元表达式分别相对于不同情景成立；如果初始序列含有两个或一个对，那么它们中的每个信息元表达式相对于一个情景成立。