Something that I sometimes find useful is to consider what's called the Curry-Howard Isomorphism: statements of logic correspond to the types of computer programs, and the statements are theorems if and only if the corresponding type is the type of a program that can actually exist.
In this correspondence, $A\to B$ represents the type of a function in a program that takes an argument of type $A$ and calculates a value of type $B$.
A function of type $A\to A$ is obviously possible, because the function just takes the $A$ that it got and gives it right back:
define function f(a) {
return a;
}
And $A\to(B\to A)$ is also possible: the function needs to take an argument of type $A$ and then give back a function of type $B\to A$. It can do this, because it can give back a second function that ignores the $B$ that it got, and that gives back the $A$ that the first function got to begin with:
define function f(a) {
define function g(b) {
return a;
}
return g;
}
But in contrast, $A\to B$ is not a theorem, because how can you write a function that gets an argument of type $A$ and gives back a result of some other, completely arbitrary type? Where could it get a $B$ from if all it has is an $A$?
The isomorphism also identifies logical AND with pairing: a value of type $A\land B$ is a pair that contains both an $A$ and a $B$, and either (or both) can be extracted. It identifies logical OR with what's called a disjoint union: A value of type $A\lor B$ is either an $A$ or a $B$, but not both, and the program can tell which of the two it is. Similarly there are interpretations for negation, for constant true and false values, and so forth.
For a more elaborate example, a program that corresponds to the theorem $\lnot\lnot(P\lor\lnot P)$,
see this answer.
The only catch is that not every classically true theorem corresponds to a program in a completely straightforward way. Some theorems of logic, such as $((A\to B)\to A)\to A$, (Peirce's law) don't correspond to a simple program. Instead they correspond to programs that use advanced features like continuations or exceptions.
Still it's often helpful to think of logical theorems as specifications for programs; if you can think of a program which performs the corresponding calculation, then the statement must be a theorem.
Viewed in this way, the statement you originally asked about, $((P\to Q)\to Q)\to Q$, seems quite unlikely: you need a function $f$ which gets an argument $x$, which is itself a function of type $(P\to Q)\to Q$, and $f$ needs to produce a value of type $Q$. If $f$ could call $x$, then $x$ would return the needed value. But it can't call $x$ because to do so it needs to give it an argument of type $P\to Q$, and it doesn't have one.
Here's the list I came up with, with the "$\subsetneq$" symbol meaning "is a proper subset of":
$(1): A = B\;$ and $\;B = C.\;$ (And hence $A = C$ by transitivity)
$(2): A = B\;$ and $\;B \subsetneq C.\;$ (And hence $A \subsetneq C$, necessarily).
$(3): A \subsetneq B\;$ and $\; B = C.\;$ (And hence, $A \subsetneq C$, necessarily).
$(4): A \subsetneq B\;$ and $\; B \subsetneq C.\;$ (And hence, $A \subsetneq C$, necessarily).
Yes, the Venn diagram for each of the four scenarios would necessarily be different, if we are distinguishing between equality of sets and "being a proper subset of" a set, so you can cover all possible relationships by drawing a Venn diagram for each case, separately.
For example, case $(1)$ would be a single circle, labeled A = B = C. Case two would be a circle A = B, contained within the larger circle C. etc...
Best Answer
First, I think you should specify what your colors mean. It is not clear to me, especially since your explanations are not 100% consistent with the diagrams.
Second, as I recall (I may be wrong), ideal Venn diagrams should have a neutral background color representing neither true nor false. That reduces any confusing implications of the diagram. (I have seen some diagrams having a pale yellow background that is both visually pleasing and not distracting.)
Assuming your white means a negative condition ("NOT"), then I believe your first diagram is explained incorrectly.
Let "a" = Has Liability Insurance Let "b" = Has Collision Insurance Then, diagram 1 shows: NOT (a AND b). That is, "NOT the drivers who are insured for (both liability and collision)", rephrased as "Drivers who are not fully ensured for both liability and collision." This is my preferred statement.
You can remove "fully" or maybe just remove "both", but if you do that you make it easier to misinterpret the diagram summary.
Alternatively, by DeMorgan's Laws, NOT (a AND b) = (NOT a) OR (NOT b) So, diagram 1 also says, "Drivers who are NOT insured for Liability OR drivers who are NOT insured for Collision."