一元算符逻辑理论三探——狭义函数相对论视野下的现代模态逻辑

万小龙，华中科技大学哲学系，湖北武汉 430074

一元算符逻辑理论三探
——狭义函数相对论视野下的现代模态逻辑

万小龙，华中科技大学哲学系，湖北武汉 430074

狭义函数相对论基本原理:对于任意二真值的逻辑变量p和由任意一元算符H与p所形成的二真值变量Hp，无论Hp是否为p的真值函数，它总会等值于p和独立于p的另一二真值变量q所形成的一个真值函数。由于有且仅有16个二真值二元函数式和有且仅有16个相应的基本二真值二元函数，所以有且仅有16个一元算符和有且仅有16个相应的基本二真值一元非函数。其他的二真值一元非函数由且仅由这16个一元算符叠置所形成。那么可进一步认为现代模态逻辑公理其实是按一阶逻辑对经典二真值函数做分类研究。模态命题逻辑中任一可能世界集W仅对应一组二元真值函数，相应的可能世界间的关系R就是这组函数共有的一种集合性质。任一公理模式在一框架内有效，就是将属于W的每个真值函数(式)按K－2分别依次代入该公理模式中的每一个“□”，使得形成一组经典定理。

狭义一元算符;经典二元真值函数;K－1;K－2

本文仅研究二真值的非函数，而把非二真值的非函数留在“3+N探”讨论。类比爱因斯坦提出“同时性的相对性原理”，本文先提出狭义函数相对论的基本原理“对于任意二真值的逻辑变量p和由任意一元算符H与p所形成的二真值变量Hp，无论Hp是否为p的真值函数，它总会等值于p和独立于p的另一个二真值变量q所形成的一个二真值函数”，简称为“非真值函数的相对性”，Hp=d(p，q)。再由此考虑二真值的现代模态命题逻辑的实质。

一、一元算符理论简述

类比爱因斯坦相对论的方法(将牛顿力学理论中作为形而上学陈述中的概念“时间”与“空间”等内化为科学理论的数学物理陈述中的可验证科学概念)，一元算符理论可以概括为:先把经典逻辑理论中作为形式系统背后的形而上学陈述的“推理有效”经过“蕴涵为真”而内化为形式体系内部的可运算的基本算符，然后再对经典联结词和逻辑真值做系统研究。

简要地说，考虑推理有效在真值语义下即蕴涵为真，从任意命题p定义作为p的蕴涵为真的结果－反(泛)函数［1］［2］①参照了［2］中第2页黄绍揆先生的称谓为逆函数。H4p－及其叠置，再用完全集{﹁，→}递归地定义出相应的其余15个算符(见表1与2)。这一方面的详细论述参见拙著“一探”［2］和“二探”［3］。

表1 一元算符真值表

表2 孪生形一元算符真值表

一元算符逻辑是直接从经典逻辑中来的，没有附加任何其它逻辑条件。所以经典逻辑具有的公理、定理和推理规则在一元算符逻辑中也都成立(在具体推理时，只要将“可真可假”看做是小于“真”却大于“假”即可，而实际分别是两个推理过程:“假”推出“假”推出“真”;“假”推出“真”推出“真”)。下文考虑多变元的情形。

表3 二变元的H4的简约真值表，当H4p=f(p，q)时，H4p'=f(p'，q)

表4 二变元的H4一般真值表，当H4p=f(p，q)时，H4p'=f(p'，q')

我们把表3和表4的两种算符形式依次记为H4－1和H4－2。

二、狭义一元算符逻辑显原形

进一步可见，H4p的真值语义与p∨q的真值语义完全相同。既然一元算符中的基本算符H4是在经典命题逻辑基础上没有增加任何其他逻辑条件而得到，所以H4p其实就是p∨q。因此，可以考虑狭义一元算符真值表中每个一元算符的一个逻辑语义都对应一个经典二元联结词。

表5 狭义一元算符真值表

表6 孪生形狭义一元算符真值表

对于一元算符真值表中另外7个带有“无真值定义”算符及它们的孪生组成的集合，我们将在考虑多值逻辑时才讨论这些算符的问题。

为了适应本文的引文，用公式A代替上面表中的变元p、A1代替上面表中的q，得到:

表7 经典二真值基本二元函数

显然，传统模态算符可能◇和必然□就分别是:H4和H3，或H'4和H'3;也即对应d2和d13，或d3和d12。而现代二真值的模态逻辑研究到今天还没有出现内含“无真值定义”的算符。因此如果狭义函数相对论能够成立，那么狭义一元算符集也即经典二元联结词集就被认为可以完备地表达模态逻辑算符。而对于任意一对HA和HB来说，当HA=f(A，A1)时，HB=f(B，A2)而不是f(B，A1)。例如，当H4A是A∨A1时，H4B是B∨A2。特设性的f(B，A1)形式对应K－1，一般形式f(B，A2)对应K－2。为了简便，下文中K－1与K－2中的“□”均先仅考虑二变元真值函数式。n为大于0的自然数时，K－(2+n)是指代人法则如上述的K－2，但考虑多于二变元的真值函数，可以看作是16个算符的叠置生成。

三、现代模态命题逻辑公理显原形

狭义函数相对论显示任意二真值的基本一元非真值函数HA总会等值于A与A1形成的16个基本二真值函数之一。如果任一模态基本命题□A属于16个HA的集合，那么只要将16个函数分别代人模态公理即可求得。以简便又常用的T公理(□A→A)为例，容易发现:

(1)T公理中的□A表示一组而非一个A的非真值函数;

(2)这一组A的非真值函数分别等值于真值函数D6、D12、D13和D16;

(3)进一步，由于公理具有的二真值特性(表示蕴涵为真或推理有效)，T公理中的□A表示的非真值函数只能等值于真值函数D6、D12、D13或D16，运用反证法不难得到证明。

(4)T公理实际上表示一组经典命题逻辑的定理:

A→A，A∧A1→A，A∧﹁A1→A，A∧﹁A→A。

对于叠置算符的语义，例如当H3A=A∧﹁A1时，H3H3A=A∧﹁A1∧﹁A1'。显然后者也是T公理中的□A，不过仅考虑16个二变元的真值函数已经能够反映模态逻辑的最基本性质。

模态命题逻辑LP16K－2:在经典命题逻辑基础上增加并仅增加的符号“□”和“◇”有且仅有明确的经典意义:“□”与任意命题(串)A组合形成的□A表示以A为一变元而形成的16个二元真值函数集(如表7)的一个子集。最大子集就是这16个真值函数的集合，最小的子集对于这16个真值函数是空集。容易算出总共有有限数量(WM+1)个不同的子集。模态公理就是在经典命题逻辑语言外仅增添了“□”或它的对偶“◇”或它们的各种叠置的公理。由于公理的特性(永真)和其中任何一个命题串的“二真值性”，任何公理中的“□”只能是至少等价于16个真值函数中的一个而不可能为“空”，所以不等价的模态公理的总数就是正好比上述子集的总数少一个即WM个。这里“□”不包括叠置算符。另外，在处理多于二变元或叠置算符时自然采用K－2形式。

LP16K－2的扩展(“□”包括叠置算符)叫做LPK－2。流行的现代模态命题逻辑叫做LPN。

LPK－2是一系列逻辑系统的总称并且有无数个“不等价”的系统和不等价的公理(下文的分析可知，由于N的限制，LPN的系统数量虽然也无数但要少的多)。“□”不包括叠置算符的流行现代模态命题逻辑叫做LP16N。

后文为了简便，除非特别指明，否则仅考虑LP16K－2和LP16N。在LP16K－2中:当□A正好表示16个真值函数的集合时，这时的模态命题逻辑公理就是经典命题逻辑的公理，相应的模态系统就是经典命题逻辑系统。而当□A表示小于16个真值函数的集合时，这时的模态公理就是一组经典命题逻辑的定理，所以相应的模态系统仍是经典命题逻辑系统(后文可知，LP16N的系统应该属于后者)。模态逻辑不过是经典逻辑的成语。模态命题逻辑系统就是经典命题逻辑系统，因此像完全性、可靠性等证明并无必要。作为一组由A为一变元形成的二变元真值函数的□A究竟是A的泛函、多值函数、复变函数、逆函数、格或其他什么由A非完全决定的东西，非要弄清楚其实也是多余。

在LPK－2或LPN中，每个模态逻辑公理中的□A都表示了一组由A为一变元形成的二真值的多变元真值函数，这才是□A作为逻辑符号所反映的思维的形式意义。在半形式语言上可以把这一组真值函数代表一集可能世界，或一堆臭皮囊，或一队分有神性的天使，甚至孙悟空的一群变身。逻辑学家(而非逻辑知识家)并无须知道“□”作为“必然”的自然意义是如何抽象为逻辑形式意义的历史［4］99－137。

每个模态公理反映其中的□A作为一组由A为一变元形成的真值函数对A的同一种集合性质。例如，LP16K－2的T公理中□A表示且仅表示A、A∧A1、A∧﹁A1和A∧﹁A对A都具有自反的性质。这一方面说明可能世界语义学中“T公理中的那一组可能世界之间具有自反性”是一种近似正确但不够准确的表述(显然，A对A∧A1并不具有自反性)，另一方面也说明像“集合论”这样的数学理论与基本逻辑理论可以是交叉关系。

由于在不同模态系统中有不同的模态公理，因此导致不同的模态公理中“□”表示的“必然”的逻辑意义不相同。虽然这些不同的公理还原为经典定理的组合后，作为其组合成分的经典定理都是等价的。这里不仅反映了“非经典逻辑仅是经典逻辑成语”的逻辑基元特性，而且揭示了整体论的形而上学起源:不同的整体由相同基元集合的不同子集形成。

在LPK－2中，虽然每个模态逻辑公理都不等价，但每个模态逻辑系统都是经典命题逻辑系统加一组经典命题逻辑中的定理，在基元意义上当然还是经典命题逻辑系统，所以都是等价的。因此说一个模态逻辑系统是另一个模态逻辑系统的扩充在上述意义上总是正确的。当然在把“□”作为个体意义时是指符合前者“□”的真值函数是要包含于后者的。

对模态命题逻辑的纯句法研究依照自然推理演绎的方法，它隐含着经典二真值语义，并自然地使用了K－2这种一般形式，因此几乎没有错误结果［5］492－502。但因为不知道“狭义函数相对性原理”，所以进展缓慢。

必然化规则N的存在使得K－2形式下各种LPN模态系统中各种定理在真值语义中的判定变得容易，不过涉及到关系语义的N的理解较为复杂，但考虑各种模态公理所反映的集合性质及其相互关系时无需考虑必然化规则的影响。

克里普克可能世界语义学是一种巧妙特设的一阶谓词逻辑语义学，在独立于K－2形式的经典二真值语义的模型时总是有效的。但当涉及像“全通性”这样的无特设性(即对应K－2形式的经典二真值语义)一阶公式时，就找不到对应的模态命题逻辑公式了。“K公理对所有模型均有效”的证明没有注意到K－2所反映的“模态算符的非完全可代入性”:f(A)如果表示A的一个真值函数，那么f(B)就表示B的同一个真值函数。但现在如果□A表示以A为一变元形成的一个二变元的真值函数，那么□B表示的是与前一个二变元的真值函数仅有相同函数式的以B为一变元形成的另一个二变元的真值函数。我们所看到的关于K公理对所有模型均有效的证明在K－2情形下都不可能成立。在杜国平的《经典逻辑与非经典逻辑基础》的第177页的19行－24行的“由［4］和［6］可得［7］”，和在李小五的《模态逻辑讲×第139的倒数第7行到倒数第5行的“u╞﹁q和u╞q”，我们认为在K－2情形下不可能成立。如果作为w对应□q和□(p→q)的真值表的同一行真值指派，即使在q和p→q真值相同时，它们的真值仍可能不同，例如后文列出的K－2时K公理对D2的无效，即这时的两个u或者其实不是同一个真值函数，或者是克里普克语义特设性地表示它们为同一个真值函数。

在可能世界语义学中，大部分模态逻辑公理都与一个一阶谓词公式对应，反之亦然。在我们对模态逻辑的理解中，每一个模态逻辑公理都与一组命题逻辑定理对应，反之亦然。这一方面说明仅从对模态逻辑做半自然半形式理解的可能世界语义学出发，很难找到甚至有时无法找到它们的一一对应;另一方面也可以解决命题逻辑与谓词逻辑的关系问题:并不是有些推理无法用命题逻辑表示才必须发展谓词逻辑，而是用谓词逻辑更方便。过去认为谓词逻辑无法还原为命题逻辑的原因是:一个谓词逻辑公式往往等价地表示一组命题逻辑公式。

本文暂不系统考虑一阶谓词逻辑LP'和相应的模态谓词逻辑LP'，但认为任何一阶谓词公式都可以用一个或一组经典命题逻辑公式等价地表示。另外，多于二元的联接词构成的二真值函数总可以还原为二元联接词构成的二真值函数。这些将在“3+N探”中细述。当然，用一篇文章还不可能(其实也无必要)准确地穷尽现代模态逻辑各种语义的每一个细节。

四、对一些重要问题的运算结果及其分析

1.K－1形式下的模态句法还原:

将16个经典二元联结词依次、分别代入上述10个典型的模态公理中的每个“□”，不难得到16张完整真值表(因为篇幅，略)和下面的总表8。

表8 典型10公理在LP16K－1形式下有效性比较表(仅用y表示有效)

表8中C公理就是经典公理，K公理是对16个经典二元联结词都有效的，但实际上在无特设性条件下的句法不可能是对应K－1。况且对于各种公理的有效性之间的互推关系有时已经过分符合现代模态逻辑的主要经典结果。例如:对称性+传递性=欧性。

K－1的模态逻辑虽然仅是“瘦身”的而非真的模态逻辑，但由于它简单，能非常明晰地反映模态逻辑的最一般本性:模态算符“□”表示共有某种集合性质的一组经典真值联接词，模态公理表示一组经典定理，所有的模态命题系统其实都等价于经典命题逻辑系统。

2.K－2形式下的模态句法还原

K－2:□A=f(A，A1)，□B=f(B，A2))，□□A=f(f(A，A1)，A1')。因为。D、T、V和Tr独立于K－1和K－2，所以只要考虑表9中余下的6个公理中有效的那些项。施反证法于6个模态公理，不是很难就算的出表9的结果。

表9 典型10公理在LP16K－2中公理模式有效性比较表(仅用y表示有效)

对自然(或必然)化规则N，如果可以把N理解为把真值函数代入□A后的真值表的每一行都要符合“A为真时，□A为真”的条件，表9中的各个公理的结果加上N与现代模态逻辑经典文本中的模态系统中仅按句法推出的结果相比较，没有发现反例。不难发现，表9中各种公理的有效性之间的互推关系也符合现代模态逻辑的主要经典结果(参见李小五:《模态逻辑讲义》，中山大学出版社，2006年.p126)。

(1)自返性⇒持续性。

(2)对称性+传递性⇒欧性。

(3)(略)

(4)自返性+欧性⇒对称性。

(5)对称性+欧性⇒传递性。

(6)对称性+传递性⇔对称性+欧性。

(7)对称性+传递性+持续性⇔自返性+欧性。

(8)自返性+对称性+传递性⇔自返性+欧性。

显然K公理不是对16个真值函数均有效(对D4、D5、D7和D10的结果还有争议)，至少对D2(或D3)即□A=A∨A1和□B=B∨A2在A、B、A1、A2取值为0、0、1、0这行无效。

3.K－2时对K－1时4、B、E、M和O公理有效项的有效性的反证法证明

又由于D1、D6、D11和D16对K－2与K－1同效，以及D2和D3那样的两个函数间的对称性，所以仅需考虑D2、D5、D13、D14、D7和D9。

(1)4公理:︱—□A→□□A

在K－1时仅对D1、D2、D3、D6、D7、D10、D12、D13、D16有效，所以现在仅需考虑 D2、D5、D7。显然在D7时，□A=A1，□□A=A1'，这时4公理无效。显然在D13时，□A=A∧A1，□□A=A∧A1∧A1'，这时4公理无效。

所以对K－2，4公理仅对D1、D2、D3、D6、D16有效。

(2)B公理:︱—A→□◇A

在K－1时仅对D1、D2、D3、D4、D5、D6、D8、D9、D11有效，所以现在仅需考虑D2、D5、D9。

D2时，□A=A∨A1，◇A=A∧﹁A1，□◇A=(A∧﹁A1)∨A1'。A→□◇A即

所以B公理在K－2时仅对D1、D4、D5、D6、D11有效。

(3)E公理:︱—◇A→□◇A

在K－1时仅对D1、D2、D3、D6有效。现在仅需考虑D2。

D2时，□A=A∨A1，◇A=A∧﹁A1，□◇A=(A∧﹁A1)∨A1'。◇A→□◇A即

(A∧﹁A1)→(A∧﹁A1)∨A1'，显然有效。

所以E公理在K－2时仅对D1、D2、D3、D6有效。

(4)M公理:︱—□◇A→◇□A

在K－1时仅对 D6、D8、D9、D11、D12、D13、D14、D15、D16有效。所以现在仅需考虑D8、D12、D14。

D8时:□A=(﹁A∨A1)∧(A∨﹁A1)，□◇A=(﹁A1∨A1')∧(A1∨A1')，◇□A= (A1∧﹁A1')∨(A1∧A1')，显然，当A1、A1'分别取1和0时，M无效。在D13时，□A=A∧A1，◇A=A∨﹁A1，□◇A=(A∨﹁A1)∧A1'，◇□A=(A∧A1)∨﹁A1'。M公理为: (A∨﹁A1)∧A1'→(A∧A1)∨﹁A1'，显然当A、A1、A1'依次取1、0、1时，M无效。D14时:□A=﹁A∧A1，◇A=﹁A∨﹁A1，□◇A=﹁(﹁A∨﹁A1)∧A1'=A∧A1∧A1'，◇□A=﹁(﹁A∧A1)∨﹁A1'=A∨﹁A1∨﹁A1'，M公理为显然有效。

所以，M公理在K－2时仅对D6、D11、D14、D15、D16有效。

(5)O公理:︱—□(□A→A)

在K－1时仅对D1、D2、D3、D6有效。所以现在仅需考虑D2。

D2时，□A=A∨A1，□A→A=A∨A1→A，□(□A→A)=(A∨A1→A)∨A1'。显然

它不是有效式。所以O公理在K－2时仅对D1、D6有效。

以下各项因为篇幅，暂略:

4.K－1条件下K公理对16个真值函数式代入的完全真值表

5.K－1条件下其他9个公理对16个真值函数式代入的完全真值表

6.K－2条件下K公理对16个真值函数式是否有效的反证法证明

7.K－2条件下K系统中必然模态算子的析取分配“不”成立的证明

8.对各个模态系统中的基本定理的经典语义证明

9.对几个认为无法找到对应一阶公式的模态公理的验算

10.对几个认为无法找到对应模态公理的一阶公式的经典命题逻辑定理的转换(待修正)

五、结论

如果由A和任意算符H所构成的二真值的非真值函数HA总是等值于一个由A作为一元而形成的一个基本经典二真值函数，那么作为二真值模态命题的“□A”就不得不仅表示一组经典二真值函数。甚至现代模态逻辑是对经典真值函数做系统分类研究的经典命题逻辑。句法上，模态命题逻辑中任一公理模式的任一“□A”都表示使得这一公理模式有效的那一组以A为一变元形成的经典多变元真值函数，任一模态公理模式是且仅是一组经典命题逻辑定理。语义上，关系语义可以还原为经典语义。但由于d(A，A1)不是A的严格意义上的函数，所以模态“□”具有非完全可代入性，即遵照K－2而非K－1的形式:K－1:当□A=d(A，A1)时，□B=d(B，A1);K－2:当□A=d (A，A1)时，□B=d(B，A2)。可能世界语义学大致曲折地反映了这种句法和语义的统一，笔者认为:一个可能世界w就是(映射)一个经典真值函数，一个世界集W就表示一组这样的真值函数，相应的可能世界间的关系R就是这组真值函数共有的集合性质。W、R和K－2式经典赋值V构成一个框架。任一公理模式在一个框架内有效，就是将属于W的那一组真值函数式按K－2规则分别依次代入该公理模式中的每一个“□”，使得形成一组经典命题逻辑定理或一个一阶谓词逻辑定理。

本文按笔者对现代模态逻辑的理解过程写作，体现了这个过程所经历的下述九步:

(1)从现代模态逻辑的一些应用(辩证逻辑、量子逻辑等)意识到需要对经典真值函数进行反(泛)函数研究。区分反函数(单值函数)和逆函数(很像多值函数)。

(2)理解“蕴涵为真”的逆函数是最基本的二真值一元算符非函数，并运用经典完全集{﹁，→}递归定义出相应的其余15个算符而形成狭义的基本二真值一元算符非函数集。

(3)发现基本的二真值一元算符非函数集就是基本经典二变元真值函数集。即16个基本二真值一元算符依次对应16个二变元二真值函数式－－非真值函数的相对性。

(4)一般的二真值一元算符非函数就是16个基本的二真值一元算符叠置所形成。

(5)模态“□A”对应一组以A为一变元形成的一组一般的二真值多变元函数。

(6)K－1与K－2的区别。

(7)任何模态命题逻辑公理都是一组经典命题逻辑定理。

(8)如果视N中的“□A”也仅具有(5)的意义，那么现代模态命题逻辑各系统在经典真值函数的基元意义上分别是经典命题逻辑系统，但在“□”的个体意义上是对经典真值函数的某些子类的分类整体研究。

(9)每个可能世界就直接对应一个经典二真值函数，但可能世界语义学除了明示了模态命题逻辑与一阶逻辑的关系，还隐含了一阶谓词逻辑与经典命题逻辑的转换关系。

回到本文的开篇，问题的关键是:二真值的Hp是否只能是16个经典二真值函数d(p，q)之一?过去逻辑学家普遍认为:Hp作为p的非真值函数，在p取一个确定真值(真或假)时，Hp的真值是不确定。但笔者认为，由于Hp是二真值的，所以当p取一个确定真值时，Hp不可能有第三种真值“真正的不确定”，它的“真假不确定”只能是确定的“真”与“假”均可。这一点从任何一个包含二真值的非真值函数的公理或定理中也可以得到印证。这样构成的作为有真值定义的“真与假的排列组合”只能是与16个经典二真值函数式一一对应。本文对可能世界语义的经典语义还原还没有完成，对必然化规则的理解还可能涉及“逻辑真与事实真”。不过无论采用何种语义，只要狭义函数相对论成立，那么至少在句法上□A只能表示一组以A为一变元所形成的多变元的经典二真值函数。笔者作为非逻辑专业的学者的严密性可能还不够，但作为科学哲学专业的教师，不禁会联想到近代物理学史上晚于经典力学出现的热质说的曾经辉煌的历史。

［1］莫绍揆:“多值函数新论”，载《南京大学学报》(自然科学版)1998年第1期。

［2］万小龙:《经典命题逻辑联结词的泛函分析初探——一元算符是否可能穷尽》，载《安徽大学学报(人文社会科学版)》2011年第6期。

［3］万小龙、李福勇、田雪:《一元算符逻辑理论二探——一元算符完全性下的道义逻辑与道义悖论研究》，载《安徽大学学报(人文社会科学版)》2012年第3期。

［4］B.Jack Copeland.“The Genesis of Possible Worlds Semantics”，Journal of Philosophical Logic 31，2002.

［5］徐明:《符号逻辑讲义》，武汉:武汉大学出版社2008年版。

On Modern Modal Logic from the Special Theory of Function Relativity

WAN Xiao-long

(Department of Philosophy，Huazhong University of Science and Technology，Wuhan430074，China)

The basic principle in the special theory of function relativity:For any two truth-valued variables p and Hp formed by any unary operator H and p，regardless of Hp is two truth-valued functions of p or not，it always be equal to a two truth-valued function formed by p and the third truth-valued variables q that is independent of p.There are only 16 truth-valued dual function formulas and only 16 unary operators and 16 corresponding basic two truth-valued non-functions.The other two truth-valued non-functions are only 16 unary operator overlay formed.Modern modal logic，in fact，is a kind of classifying study on classical two truthvalued functions in terms of first order logical axioms and rules.In modal propositional logic，any set of possible worlds W only means a set of a truth-function with two variables，and the corresponding relations between possible worlds R is a set property which the set of truth-functions have in common.And the validity of any axiom schema in a framework is just that every truth-function formula with two variables belonging to W is，in turn，substituted in each“□”of the axiom schema respectively such that a set of classical theorems are formulated.

non-truth-function;modal axiom schemas;K－1;K－2

B81

A

1671-7023(2012)03-0033-07

万小龙(1964－)，男，江苏常州人，华中科技大学哲学系教授、博士生导师，国家马克思主义工程“科学技术哲学”首席专家，研究方向为科学哲学、量子力学哲学与逻辑哲学。

国家留学基金(学号200635015)项目;国家社科基金项目(2007zxc49)

2012-04-13

责任编辑吴兰丽