A proof-theoretical investigation on diagrammatic reasoning

最近，基于图示或图形表示的逻辑推理受到了各个领域的研究人员的关注。对于图解推理的研究，将传统符号逻辑和认知科学的方法和分析结合起来是非常重要的。在这类研究中，迄今为止的研究主要集中在对图的静态性质的语义研究上，即在表征层面上的性质。在这项研究中，我引入了一个证明论框架来考察图形表征的动态特性，特别是欧拉图和维恩图的动态特性。然后，我通过应用逻辑翻译的基本证明论技巧之一，在我的证明论框架中形式化了“搭便车”的概念。搭便车是图表最基本的性质之一，在认知科学文献中主要讨论图表的推理效能。然后，在顺风车形式化的基础上，研究了Euler图形化证明和Venn图形化证明结构的证明论特征，并与传统符号逻辑中常用的自然演绎证明进行了比较。

Recently, logical reasoning based on diagrammatic or graphical representations has been investigated by researchers from various areas. For the study of diagrammatic reasoning, it is important to combine methods and analyses of traditional symbolic logic and cognitive science. In such studies, researches so far have concentrated on semantic studies on the static nature of diagrams, i. e., the nature at the level of representation. And there are few proof-theoretical investigations on the dynamic nature of diagrams, i. e., the nature at the level of proofs or at the level of manipulation of diagrams.In this study, I introduced a proof-theoretical framework to investigate the dynamic nature of diagrammatic representations, in particular of Euler and Venn diagrams. Then, I formalized, by applying one of the basic proof-theoretical techniques of logic translation, the notion of "free ride" in my proof-theoretical framework. Free ride is one of the most basic properties of diagrams that is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. Then, based on the formalization of free ride, I investigated a proof-theoretical characterization of the structure of Euler diagrammatic proofs and that of Venn diagrammatic proofs, compared with the usual natural deduction proofs of the traditional symbolic logic.