Counter-example construction with Euler diagrams (Q495828)

Recently, some visual manipulations of graphic objects have been studied systematically from the view points of logic and computer science, as can be seen in [The language of first-order logic. Including the IBM-compatible Windows version of Tarski's World 4. 0. 3rd ed. Stanford, CA: Stanford University, Center for the Study of Language and Information (1992; Zbl 0942.03500)] by \textit{J. Barwise} and \textit{J. Etchemendy}, [Fundam. Inform. 46, No. 1--2, 1--29 (2001; Zbl 0974.68206)] by \textit{A. G. Cohn} and \textit{S. M. Hazarika}, [``A spatial logic based on regions and connection'', in: Proceedings of 3rd international conference on knowledge representation and reasoning. San Mateo: Morgan Kaufmann. 165--176 (1992)] by \textit{D. A. Randell} et al., and so on. Euler diagrams were originally introduced in the 18th century as a graphic representation of syllogisms. In their previous works, the author of this paper and others formalized Euler diagrams as well as their visual manipulations for syllogisms into a purely syntactical deductive system and developed a so-called proof-theoretic analysis on it, which includes among others its completeness with respect to the natural set-theoretic semantics proved by the method of canonical ``diagrammatic proof'' construction. The main issue of this paper is to show that the counterexample construction like proof-search or tableaux in logic is also available by a similar proof-theoretic method of canonical ``counter-diagrammatic proof'' construction to those unprovable in the former system under certain restriction which however is still sufficient for the original representation of syllogisms. Thus, the result not only gives rise to an alternative exposition of completeness without referring to any semantical means, but would also be interpreted as to establish the decidability of ``syllogisms thus represented by Euler diagrams''.