A proof-theoretical investigation on diagrammatic reasoning

近年来，基于图解或图形表示的逻辑推理得到了各个领域的研究人员的研究。将传统符号逻辑的方法和分析方法与认知科学相结合，是图解推理研究的重要内容。在这些研究中，迄今为止的研究主要集中在对图的静态性质的语义研究，即表征层面的性质。而对于图的动态性，即图在证明层面或图的操作层面的动态性，很少有证明理论的研究。在这项研究中，我引入了一个证明理论框架来研究图解表示的动态性质，特别是欧拉图和维恩图。然后，我运用逻辑翻译的一种基本理论证明技术，在我的理论证明框架中形式化了“搭便车”的概念。“搭便车”是图表最基本的属性之一，认知科学的文献主要讨论图表的推理效能。然后，基于搭便车的形式化，我研究了欧拉图证明和维恩图证明结构的证明理论表征，并与传统符号逻辑中通常的自然演绎证明进行了比较。

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.