Venn diagrams and Categorical Propositions in F#

Categorical propositions express specific relations between elements of different sets, in term of quantifier which can be Universal (like All, or None), or Particular (Some); and positive or negative ("is" or "is not").

Examples: All Mammals are Animals, No Mineral is Alive, Some people are Smart, Some people are Not Smart.
In this post I am going to show some code in F# I wrote, representing categorical propositions, and particularly, related to the union of them, with an internal structure that reflects the representation based on Venn diagrams.
This can be used to verify in an automated way the compatibility between different propositions, in the same way we use simple rules by Venn diagrams.
Example: "All S is P" and "Some S is not P" are not compatible. Venn diagrams show in this case that the two diagrams can't be overlapped.
The area of the diagrams can only be blank, can have a '*' or can be blackfilled, but we can't have '*' (meaning: there is something here), and a black area (meaning: there is nothing here), at the same time.

The building blocks are the four basic form of categorical propositions, and are classified as Affirmative or Negative, and Universal or Particular, as follows:

They have representation based on Venn diagrams:

Venn diagrams in this case consist on two circles indicating two sets which are partially overlapped, so they form three regions. The left region indicates what is in S that is not in P, in the middle region what is in common between them, and on the right what is in P that is not in S.
To indicate that a region is empty we have to black-color it, and to indicate that in a region there must be something in it we have to put an asterisk in it. It is not possible to black-color and put an asterisk to a region at the same time because it will lead to a contradiction (like "All S is P" and "Some S is not P" which is impossible).

Symmetric basic form diagrams (E and O) represent proposition that are valid also on the reverse: so Some S is P means also Some P is S, and No S is P means also No S is P.

As long as we avoid placing asterisk and black-color in the same area (which leads to a contradiction) we can have more complex and valid (consistent) diagrams than the basic forms, which represent more proposition for example as follows:

This diagram means: Some S is not P, No S is P, No P is S, and Some P is not S.

I want to write some F# code solving the problem of translating any Venn diagram like the previous one, involving two sets, in the list of all the categorical propositions that follow from it.

I'll use records to represent either the diagram and either a categorical proposition.
To explain what I will get, this is a possible automated NUnit test related to the "A" proposition:

[<Test>]
    let ``A Venn diagram to proposition``()=
        let allSIsP = {S=BlackFilled; SP=Empty;P=Empty}
        let expectedProposition = [{quantifier1=All;category1=S;appartenence=Is;category2=P}]
        let actual = VennToPropositions allSIsP
        Assert.AreEqual(expectedProposition,actual)

I need to define:
a type for any diagram involving two categories, which will be a record:

type twoSetsVennDiagram = {S: SectionStatus; SP: SectionStatus; P: SectionStatus}

A "SectionStatus" to set each of its region with the appropriate status:

type SectionStatus = Empty | BlackFilled | Starred

A "Propositions" type (again, as a record):

type twoTermsProposition = {quantifier1: Quantifier; category1: CategoryRef; appartenence: Appartenence; category2: CategoryRef}

Quantifier will be:

type Quantifier = All | Somes | No

("Some" is an F# keyword, so to avoid confusion I chose "Somes")

Appartenence (i.e. "belonging") will be:

type Appartenence = Is | IsNot

CategoryRef will simply be a possible name of the set involved:

type CategoryRef = S | M | P 

("S", "M", "P" are typical names used to model categorical propositions and syllogisms  - which I'm not going to write about this time, so they are just "typical names" given to sets involved in categorical forms. For instance in the classical syllogism "Socrates is human, all humans are mortal, Socrates is Mortal, S is Socrates (or "everything that is Socrate"), M is "everything that is human" and P is "everything that is mortal").


The implementation aimed just to pass this test is like:

let VennToPropositions diagram = [{quantifier1=All;category1=S;appartenence=Is;category2=P}]

I expect that I need a sort of lookup table for basic diagrams (with only one non empty region, having BlackFilled or Starred state), and that I can one step a time add an element to such lookup on the base of adding a new test against the case:

       


let VennToPropositions diagram =

    match diagram with 

        | {S=Empty; SP=Empty;P=Empty} -> []

        | {S=BlackFilled; SP=Empty;P=Empty} ->  [{quantifier1=All;category1=S;appartenence=Is;category2=P}]

        | {S=Empty; SP=Empty;P=BlackFilled} ->  [{quantifier1=All;category1=P;appartenence=Is;category2=S}]

        | {S=Empty; SP=BlackFilled;P=Empty} ->  [{quantifier1=No;category1=S;appartenence=Is;category2=P};{quantifier1=No;category1=P;appartenence=Is;category2=S}]

        | {S=Empty; SP=Starred;P=Empty} -> [{quantifier1=Somes;category1=S;appartenence=Is;category2=P};{quantifier1=Somes;category1=P;appartenence=Is;category2=S}]

        | {S=Starred; SP=Empty;P=Empty} -> [{quantifier1=Somes;category1=S;appartenence=IsNot;category2=P}]

        | {S=Empty; SP=Empty;P=Starred} -> [{quantifier1=Somes;category1=P;appartenence=IsNot;category2=S}]






       
 

Basically the cases that are considered in this "lookup" table are the four basic forms, their "reverse", and the completely empty one, and the reverse of the ones that are not symmetrical:

But the match against more complex diagrams is missing, as the following:


I can see that this diagram is the union of the following basic forms:

The resulting proposition is the union of them.

(Extreme case:  when all the region are filled.
The result may looks weird: "All M is P - No M is P - No P is M  - All P is M", but it can be sound anyway, because it applies when M and P are both empty: the "All" quantifier does not commit to existence, but the "Some" does).

The related test to a function that decomposes it could be as follows:

[<Test>]
    let ``complex decomposition``()=
         let SomeSIsNoP = {S=Starred; SP=BlackFilled;P=Starred}
         let actual = basicCategoricalDecomposition SomeSIsNoP
         let expected = [{S=Starred;SP=Empty;P=Empty};{S=Empty;SP=BlackFilled;P=Empty};{S=Empty;SP=Empty;P=Starred}]
         Assert.AreEqual(expected,actual)

So, any diagram that is more complex than those six forms, can still be decomposed in basic forms, then they can be matched returning the basic propositions, and then all the propositions can be joined together.

The basicCategoricalDecomposition function is:

       



let basicCategoricalDecomposition diagram =

        match diagram with

            | {S=s_pattern; SP=Empty;P=Empty}  when s_pattern <> Empty -> [{S=s_pattern; SP=Empty;P=Empty}] // A or O

            | {S=Empty; SP=sp_pattern;P=Empty} when sp_pattern <> Empty -> [{S=Empty; SP=sp_pattern;P=Empty}]    // E or I  

            | {S=Empty; SP=Empty;P=p_pattern} when p_pattern <> Empty -> [{S=Empty; SP=Empty;P=p_pattern}]

            | {S=s_pattern; SP=sp_pattern;P=Empty} -> [{S=s_pattern; SP=Empty; P=Empty};{S=Empty;SP=sp_pattern;P=Empty}]

            | {S=Empty; SP=sp_pattern;P=p_pattern} -> [{S=Empty; SP=sp_pattern; P=Empty};{S=Empty;SP=Empty;P=p_pattern}]

            | {S=s_pattern; SP=Empty;P=p_pattern} -> [{S=s_pattern; SP=Empty; P=Empty};{S=Empty;SP=Empty;P=p_pattern}]

            | {S=s_pattern; SP=sp_pattern;P=p_pattern} -> [{S=s_pattern;SP=Empty;P=Empty};{S=Empty;SP=sp_pattern;P=Empty};{S=Empty;SP=Empty;P=p_pattern}]

            | _ -> []


       
 

So far if the VennToProposition matches a basic diagram it works as a lookup table.
If I pass is is a more complex diagram, then any match fails, and so I add a default matching rule that just calls the above basicCategoricalDecomposition diagram by a recursive call to get the union of all the propositions.

I rewrite here the complete VennToProposition function:

       


let rec VennToPropositions diagram =

    match diagram with 

        | {S=Empty; SP=Empty;P=Empty} -> []

        | {S=BlackFilled; SP=Empty;P=Empty} ->  [{quantifier1=All;category1=S;appartenence=Is;category2=P}]

        | {S=Empty; SP=Empty;P=BlackFilled} ->  [{quantifier1=All;category1=P;appartenence=Is;category2=S}]

        | {S=Empty; SP=BlackFilled;P=Empty} ->  [{quantifier1=No;category1=S;appartenence=Is;category2=P};{quantifier1=No;category1=P;appartenence=Is;category2=S}]

        | {S=Empty; SP=Starred;P=Empty} -> [{quantifier1=Somes;category1=S;appartenence=Is;category2=P};{quantifier1=Somes;category1=P;appartenence=Is;category2=S}]

        | {S=Starred; SP=Empty;P=Empty} -> [{quantifier1=Somes;category1=S;appartenence=IsNot;category2=P}]

        | {S=Empty; SP=Empty;P=Starred} -> [{quantifier1=Somes;category1=P;appartenence=IsNot;category2=S}]

        | _ -> List.fold (fun acc item -> acc @ (VennToPropositions item) ) [] (basicCategoricalDecomposition diagram)



      
 

This last line is the one which decomposes in basic forms and then call recursively the VennToPropositions.

So far, any valid two sets Venn diagram corresponds to a set of one or more basic categorical propositions consistent each other.
Using the Fsharp Repl it is possible to test immediately the code, or it is possible to write new tests.
If needed, the sources are available on gitHub.

The page 184 of "Understanding Arguments" provides problems that can be solved using this "VennToPropositions" function (but of course they are not supposed to be solved with an automated tool).

Possible extension can be about evaluating categorical syllogisms, i.e. particular inferences involving two categorical propositions and three sets, but it can be something for another post.