Set Venn Diagrams Applied to Inclusions and Non-inclusions

摘要

In this work, formulas are inclusions (t_1 subseteq t_2) and non-inclusions (t_1not subseteq t_2) between Boolean terms (t_1) and (t_2). We present a set of rules through which one can transform a term t in a diagram (Delta t) and, consequently, each inclusion (t_1 subseteq t_2) (non-inclusion (t_1not subseteq t_2)) in an inclusion (varDelta t_1 subseteq varDelta t_2) (non-inclusion (varDelta t_1 not subseteq varDelta t_2)) between diagrams. Also, by applying the rules just to the diagrams we are able to solve the problem of verifying if a formula (varphi ) is consequence of a, possibly empty, set (varSigma ) of formulas taken as hypotheses. Our system has a diagrammatic language based on Venn diagrams that are read as sets, and not as statements about sets, as usual. We present syntax and semantics of the diagrammatic language, define a set of rules for proving consequence, and prove that our set of rules is strongly sound and complete in the following sense: given a set (varSigma cup varphi ) of formulas, (varphi ) is a consequence of (varSigma ) iff there is a proof of this fact that is based only on the rules of the system and involves only diagrams associated to (varphi ) and to the members of (varSigma ).