Intuitionistic Euler-Venn Diagrams
Sven Linker
Abstract.
We present an intuitionistic interpretation of Euler-Venn diagrams with respect to Heyting algebras. In contrast to classical Euler-Venn diagrams, we treat shaded and missing zones differently, to have diagrammatic representations of conjunction, disjunction and intuitionistic implication. Furthermore, we need to add new syntactic elements to express these concepts. We present a cut-free sequent calculus for this language, and prove it to be sound and complete. Furthermore, we show that the rules of cut, weakening and contraction are admissible.
Thanks for the talk Sven. Do you have plans to evaluate the effectiveness of this new diagrammatic logic? It would be interesting to investigate whether it is more effective for people, say in terms of ability to accurately interpret the diagrams, than symbolic counterparts.
Hi Gem,
it would be great to examine this! I assume that designing a study will be hard for a few reasons though. It is not immediately clear to me, what kind of people are the right target demographic.
If we investigate how participants without any (or much) experience in constructive reasoning understand/use the diagrams, then the training part of a study would take a lot of time and effort. But if the targets are participants with experience in reasoning with constructive logics they could be biased (since they probably spent much time with the symbolic logic already).
So, it would be important to be very careful in carving out the purpose of such an experiment.
Unfortunately, I will probably not have access to a large enough pool of participants to do such a study in the near future (I will start a new job in September). But if you (or potential PhD students/postdocs of yours) are interested in collaborating on such a study, please let me know!