Abstract
Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us to formalize and analyze free ride in terms of proof theory. The notion of normal form of Euler diagrammatic proofs is investigated, and a normalization theorem is proved. Some consequences of the theorem are further discussed: in particular, an analysis of the structure of normal diagrammatic proofs; a diagrammatic counterpart of the usual subformula property; and a characterization of diagrammatic proofs compared with natural deduction proofs.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Allwein, G., and J. Barwise (eds.), Logical Reasoning with Diagrams, Oxford Studies in Logic and Computation Series, 1996.
Barwise, J., and J. Seligman, Information Flow: The Logic of Distributed Systems, Cambridge University Press, 1997.
Buss, S. R., Propositional proof complexity: an introduction, in U. Berger and H. Schwichtenberg (eds.), Computational Logic, Springer, Berlin, 1999 pp. 127–178.
Gentzen, G., Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39:176–210, 405–431, 1934. English Translation: Investigations into logical deduction, in M. E. Szabo (ed.), The collected Papers of Gerhard Gentzen, 1969.
Howse, J., G. Stapleton, and J. Taylor, Spider diagrams, LMS Journal of Computation and Mathematics 8:145–194, 2005, London Mathematical Society.
Mineshima, K., M. Okada, and R. Takemura, Conservativity for a hierarchy of Euler and Venn reasoning systems, Proceedings of Visual Languages and Logic 2009, CEUR Series 510:37–61, 2009.
Mineshima, K., M. Okada, and R. Takemura, A diagrammatic inference system with Euler circles, accepted for publication in Journal of Logic, Language and Information.
Mineshima, K., M. Okada, and R. Takemura, Two types of diagrammatic inference systems: natural deduction style and resolution style, in Diagrammatic Representation and Inference: 6th International Conference, Diagrams 2010, Lecture Notes In Artificial Intelligence, Springer, 2010, pp. 99–114.
Mossakowski T., Diaconescu R., Tarlecki A.: What is a logic translation?. Logica Universalis 3(1), 95–124 (2009)
Negri, S., and J. von Plato, Structural Proof Theory, Cambridge, UK, 2001.
von Plato, J., Proof theory of classical and intuitionistic logic, in L. Haaparanta (ed.), History of Modern Logic, Oxford University Press, 2009, pp. 499–515.
Prawitz, D., Natural Deduction, Almqvist & Wiksell, 1965 (Dover, 2006).
Prawitz, D., Ideas and results in proof theory, in Proceedings 2nd Scandinavian Logic Symposium, 1971, pp. 237–309.
Shimojima, A., On the efficacy of representation, Ph.D thesis, Indiana University, 1996.
Shin, S.-J., The Logical Status of Diagrams, Cambridge University Press, 1994.
Stapleton G.: A survey of reasoning systems based on Euler diagrams, in Proceedings of Euler 2004. Electronic Notes in Theoretical Computer Science 134(1), 127–151 (2005)
Stapleton G., Howse J., Rodgers P., Zhang L.: ZhangGenerating Euler Diagrams from existing layouts, Layout of (Software) Engineering Diagrams 2008. Electronic Communications of the EASST 13, 16–31 (2008)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Takemura, R. Proof Theory for Reasoning with Euler Diagrams: A Logic Translation and Normalization. Stud Logica 101, 157–191 (2013). https://doi.org/10.1007/s11225-012-9370-6
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-012-9370-6