存在图是查尔斯·皮尔士发明的逻辑表达式的一种图示或可视表示法。皮尔士在1882年写了第一篇关于图形逻辑的论文,并持续开发这种方法直到1914年他故去。
图形皮尔士提出了三个存在图系统:
alpha,同构于命题演算和两元素布尔代数;
beta, 同构于所有公式都闭合的有等式的一阶逻辑;
gamma, (几乎)同构于普通模态逻辑。
Alpha嵌套于beta和gamma中。Beta不嵌套于gamma中,量化的模态逻辑超出了皮尔士的视野。
Alpha语法是:
空白页;
写在页面任何地方的单一的字母或短语;
包围在叫做切或sep的简单闭合曲线内的对象(子图)。切可以为空。切可以随意嵌套和毗连但不能交叠。一个图的任何合式部分都是子图。
语义是:
空白页指示真理;
字母,短语,子图和整个图可以为真或假;
用切包围一个对象等价于逻辑否定或布尔补运算。所以空切指示假;
在一个给定切内的所有对象都默认的合取起来了。所以alpha图是极小表示的句子逻辑,基于了对与和非的充分表达。alpha图创建了对二元素布尔代数和真值函子的根本简化。
一个对象的深度是包围它的切的数目。
推理规则:
插入 - 任何图都可以插入到奇数层。
删除 - 任何图都可以删除自偶数层。
等价规则:
重切 - 嵌套的成对的切可以被增加或去除自任何图的周围。
重复 - 任何子图都可以重复出现在包含这个子图的那个图中的任何地方。
去重复 - 任何图内重复出现的两个子图可以去掉同层中任何一个或位于内层的那个子图1。
证明按照一系列步骤操纵一个图,每个步骤都由上述规则中一个来证实,直到这个图被简约为一个空切或空白页。可以如此简约的图现在叫做重言式或矛盾。不能简约超过一个特定点的图类似于一阶逻辑的可满足公式。
Beta皮尔斯使用直觉的英语短语来记号表示谓词;还采用了当代逻辑使用的大写拉丁字母。点断言包含在论域中的一个个体的存在。同一个对象的多个实例用线连起来,这个线叫做"同一线"。这里没有文字变量或量词。连接两个或多个谓词的同一线共享一个公共变量。beta图可以被当作采用可隐含量化的变量。对象的深度是它包含的切的数目。如果一个变量的"最浅"的实例有偶数(奇数)深度,这个变量被默认的存在(全称)量化了。beta图看起来是流线型的带有等式的一阶逻辑,但是在次要文献中没有清晰的指出。
Gamma向alpha增加了第二类切,写做虚线而不是实线。使用虚线的简单闭合的曲线可以读做模态逻辑的基本一元运算。
beta图同构于谓词演算;
gamma图的直接修正得到周知的模态逻辑S4和S5。所以gamma图可以看作特异形式的正规模态逻辑。Zeman的这个发现值得注意。
本词条内容贡献者为:
王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所