Set Venn Diagrams Applied to Inclusions and Non-inclusions

摘要

In this work, formulas are inclusions t_1 is contained in t_2 and non-inclusions t_1 (is contained in) 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 Δt and, consequently, each inclusion t_1 is contained in t_2 (non-inclusion t_1 (is contained in) t_2) in an inclusion Δt_1 is contained in Δt_2 (non-inclusion Δt_1 (is contained in) Δ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 φ is consequence of a, possibly empty, set Σ 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 Σ ∪ φ of formulas, φ is a consequence of Σ iff there is a proof of this fact that is based only on the rules of the system and involves only diagrams associated to φ and to the members of Σ.