m2[]:=DynamicModule[{sym,expr, expr2, pad1,pad2,pad3},
Panel@Dynamic@Column[{
Column[{Multicolumn[pad1,{Automatic,10},Appearance->"Horizontal",ItemSize->Automatic],
Multicolumn[pad2,{Automatic,5},Appearance->"Horizontal",ItemSize->Automatic],
Multicolumn[pad3,{Automatic,5},Appearance->"Horizontal",ItemSize->Automatic]},Dividers->{All,Gray}],


Grid[Transpose[{"S"<>StringJoin[#,":  "]&/@(ToString/@Range[Length[StringSplit[StringJoin[expr],{"\n"}]]]),StringSplit[StringJoin[expr],{"\n"}]}],Background->{{LightGreen,White}},Dividers->Center],
"\nEnglish Translation",
Grid[Transpose[{"S"<>StringJoin[#,":  "]&/@(ToString/@Range[Length[StringSplit[StringJoin[expr2],{"\n"}]]]),StringSplit[StringJoin[expr2],{"\n"}]}],Background->{{LightGreen,White}},Dividers->Center]
}],
Initialization:>(
assoc=<|
"quants"->{"∀","∃","∄"},
"member"->{"∈","∉"},
"subset"->{"⊂","⊆","⊄"},
"space"->{Style["␣",Black]},
"enter"->{Style["⌤",Blue]},
"del"->{Style["⌫",Red]},
"clear"->{"C"},
"seperators"->{", ",":","(",")","[","]","{","}"},
"suchthat"->{"\[VerticalSeparator] "},
"logic"->{"∧","∨","⟺","⟹","¬","T","F"},
"arith"->{"+","-","\[Cross]","/",">","⩾","<","⩽"},
"eq"->{"=","≡"},
"digits"->ToString/@Range[0,9]~Join~{".","±","∓","\[VerticalSeparator]","≈","∝"},
"sets"->{"ℕ","ℤ","ℚ","ℂ","ℝ","∅","∞","(Subscript[ℵ, 0])","(Subscript[ℵ, 1])","(2^(Subscript[ℵ, 0]))"},
"powerset"->{"𝒫"},
"∀"->{"for every","for all"},
(* reverse associations *)
"∃"->{"for some"},
"∄"->{"for no"},
"∈"->{"belongs to", "member of"},
"∉"->{"belongs not to","not a member of"},
"⊂"->{"subset of"},
"⊆"->{"subset of or equal to"},
"⊄"->{"not a subset"},
"∧"->{"And"},
"∨"->{"Or"},
"⟹"->{"Implies","Therefore"},
"⟺"->{"if and only if"},
"¬"->{"Not"},
"T"->{"True"},
"F"->{"False"},
"\[VerticalSeparator] "->{"such that"},
":"->{"such that"},
"𝒫"->{"Set of All Subsets"}
|>;
sample1="positive Integers Real positive negative for every number such that set of any some then if true false there is are since therefore is";
words=<|"general"->Sort@(StringJoin[#," "]&/@(DeleteDuplicates[StringSplit[sample1]]))|>;


sym={"p","q","r","x","y","z",ToString["x"^2,TraditionalForm],ToString["y"^2,TraditionalForm],ToString[Sqrt["x"^2+"y"^2],TraditionalForm],ToString[Sqrt[""],TraditionalForm]};
expr={" "};
expr2={" "};
pad1=(Button[#,AppendTo[expr,#];AppendTo[expr2,RandomChoice@assoc[#]<>" "],Appearance->"Palette"]&/@assoc["quants"])~Join~
(Button[#,AppendTo[expr,#];AppendTo[expr2,RandomChoice@assoc[#]<>" "] ,Appearance->"Palette"]&/@assoc["member"])~Join~
(Button[#,AppendTo[expr,#];AppendTo[expr2,RandomChoice@assoc[#]<>" "],Appearance->"Palette"]&/@assoc["subset"])~Join~
(Button[#,AppendTo[expr,#];AppendTo[expr2,#],Appearance->"Palette"]&/@assoc["sets"])~Join~
(Tooltip[Button[#,AppendTo[expr,#];AppendTo[expr2,RandomChoice@assoc[#]<>" "],Appearance->"Palette"],"Power Set"]&/@assoc["powerset"])~Join~
(Button[#,AppendTo[expr,#];AppendTo[expr2,RandomChoice@assoc[#]<>" "],Appearance->"Palette"]&/@assoc["logic"])~Join~
(Button[#,AppendTo[expr,ToString[#,StandardForm]];AppendTo[expr2,ToString[#,StandardForm]<>" "],Appearance->"Palette"]&/@(sym))~Join~
(Button[#,AppendTo[expr,#];AppendTo[expr2,#],Appearance->"Palette"]&/@assoc["arith"])~Join~
(Button[#,AppendTo[expr,#],Appearance->"Palette"]&/@assoc["eq"])~Join~
(Button[#,AppendTo[expr,#];AppendTo[expr2,#];,Appearance->"Palette"]&/@assoc["seperators"])~Join~
(Button[#,AppendTo[expr,#];;AppendTo[expr2,RandomChoice@assoc[#]<>" "];,Appearance->"Palette"]&/@assoc["suchthat"])~Join~
(Tooltip[Button[#,AppendTo[expr," "];AppendTo[expr2," "],Appearance->"Palette"],"Space"]&/@assoc["space"])~Join~
(Tooltip[Button[#,AppendTo[expr,"\n "];AppendTo[expr2,"\n "],Appearance->"Palette"],"New Line"]&/@assoc["enter"])~Join~
(Tooltip[Button[#,If[Length[expr]>0,expr=Delete[expr,-1];expr2=Delete[expr2,-1]],Appearance->"Palette"],"Delete"]&/@assoc["del"])~Join~
(Tooltip[Button[#,expr={" "};expr2={" "},Appearance->"Palette"],"Clear All"]&/@assoc["clear"]);

pad2=(Button[#,AppendTo[expr,#];AppendTo[expr2,#],Appearance->"Palette"]&/@assoc["digits"]);
pad3=(Button[#,AppendTo[expr,#];AppendTo[expr2,#],Appearance->"Palette"]&/@words["general"]);)

]


m3[]:=DynamicModule[{p,q,f,data},
Dynamic@Panel@Column[{
Button["Again",
{p,q}=RandomChoice@data;],

Multicolumn[Table[RegionPlot[f[p,q],{x,-2,2},{y,-2,2},PlotLabel->StringReplace["p(x,y)="<>ToString[p,TraditionalForm]<> "\nq(x,y)="<>ToString[q,TraditionalForm]<>"\n\!\(TraditionalForm\`∀ \\ x \(TraditionalForm\`\(\(∀ \\ y\)\(,\)\)\)\)p(x,y)"<>ToString@f<>"q(x,y)",{"And"->"∧","Or"->"∨","Xor"->"⊻","Implies"->"\[Implies]","Nand"->"⊼","Nor"->"⊽"}]],{f,{And,Or,Xor,Implies,Nand,Nor}}], {2,Automatic},Frame->All,FrameStyle->Directive[Orange,Thickness[2],Dashing[4]]]
}]
,
Initialization:>(
data={{(((-(1/2)+x))^2)+(y^2)<1,((((1/2)+x))^2)+(y^2)<1},
{1/4≤x^2+y^2≤1&&y≥0,y≥-x},
{1/4≤x^2+(2y)^2,x^2+(2y)^2≤1},
{x^2+y^3<2,x+y<1},
{x^2<y^3+1,y^2<x^3+1},
{x≤2y+1,y>x-1}};
{p,q}=RandomChoice@data;
)
]



m4[]:=DynamicModule[{p,q,f,data},
Dynamic@Panel@Column[{
Button["Again",
{p,q}=RandomChoice@data;],

Multicolumn[Table[RegionPlot3D[f[p,q],{x,-3,3},{y,-3,3},{z,-3,3},PlotLabel->StringReplace["p(x,y)="<>ToString[p,TraditionalForm]<> "\nq(x,y)="<>ToString[q,TraditionalForm]<>"\n\!\(TraditionalForm\`∀ \\ x \(TraditionalForm\`\(\(∀ \\ y\)\(,\)\)\)\)p(x,y)"<>ToString@f<>"q(x,y)",{"And"->"∧","Or"->"∨","Xor"->"⊻","Implies"->"\[Implies]","Nand"->"⊼","Nor"->"⊽"}],Mesh->None,PlotPoints->50,PlotStyle->Directive[Yellow,Opacity[0.7]]],{f,{And,Or,Xor,Implies,Nand,Nor}}], {2,Automatic},Frame->All,FrameStyle->Directive[Orange,Thickness[2],Dashing[4]]]
}]
,
Initialization:>(
data={{1≤x^2+y^2+z^2≤3,y≥0},
{x<2y+z+3,y>x+2z-4},
{x^2+y^2+z^2<1,x^2+y^2<z^2}
};
{p,q}=RandomChoice@data;
)
]

CDFDeploy[ToFileName[{$UserDocumentsDirectory},"Set_Theory_Quantifiers.cdf"],
expr=Column[{
Pane@1.2.1. Statements involving variables
,
Spacer[100],
Pane@The sentence “x + 2 = 5” cannot be assigned a truth value and so it is technically not a statement. However, if we knew the value of x we could determine its truth value. We say that it is a statement involving a variable, namely x. If we allow x to have value 3 then we get a true statement whereas, if we let x have value 1 we get a false statement. Symbolically, we might represent the above statement as p(x). We see that p(3) is true while p(1) is false. Similarly, the statement xy = 4 could be represented symbolically as q(x,y) since it is a statement involving two variables. Again, to assign a truth value to q(x,y) we would have to know the values of both x and y. If x had value 2 and y had value 5 then q(2,5) would have truth value F. Note that q(2,2) has truth value T.

Another way to be able to assign truth values to statements involving variables is through the use of quantifiers. 

Definition 1.2.1.1. The universal quantifier, ∀ , in English means “For all possible values of the variable”.

Definition 1.2.1.2. The existential quantifier, ∃ , in English means “There is a value of the variable”. 

Thus, with the examples above, the following are statements: ∀ x, p(x);  ∃ x p(x). The first states that for all possible values of the variable x that x + 2 = 5. The second states that there is a value of x for which x + 2 = 5. Clearly, we have made each of these a statement (and we might believe the first to be false and the second to be true). The problem we are left with is what do we mean by the possible values of the variable? 

Definition 1.2.1.3.  "There is one and only one" is used to indicate that exactly one object with a certain property exists. In mathematical logic, this sort of quantification is known as uniqueness quantification or unique existential quantification. It  is often denoted with the symbol ∃!.

For example the formal statement: ∃! n∈ℕ, n - 3 = 6

It may be read aloud as "there is exactly one natural number n such that n - 3 = 6". 

Definition 1.2.1.4. We assume that the variable in our statement may be replaced by a quantity from a set of known objects. This set of objects is called the universal set of discourse, or more briefly, the universal set.

Usually, this universal set will be understood from the context. However, if necessary, we shall define the universal set for each variable in the statement and write something like ∀ x∈U, p(x). Here, the notation x∈U translates into English as “x an element of the set U”. Note that for quantified statements involving more than one variable, the universal set for each variable may be different.

Alternatively, we may think about a statement involving variables as a statement about the universal set U. 

Definition 1.2.1.5. The truth set of the statement consists of those elements of U for which the statement is true. 

For example, if the universal set is the set of integers then the truth set of the statement “(x^2)=4” is -2,2 . A statement about U is a tautology if and only if its truth set is U and a contradiction if its truth set is the empty set. Thus a statement such as ∀ x∈U, p(x) is true if its truth set is U. If its truth set is a proper subset of U then it is a false statement. A statement of the form ∀ x∈U, p(x) is true if its truth set is non empty and false if its truth set is the empty set.

Let us consider an example called Loving Relation as an example of usage quantifiers.

English sentences like "everyone loves someone" can be formalized by first-order logic formulas like ∀x ∃y L(x,y). This is accomplished by abbreviating the relation "x loves y" by L(x,y). Using just the two quantifiers ∀ and ∃ and the loving relation symbol L, but no logical connectives and no function symbols (including constants), formulas with 8 different meanings can be built. The following diagrams show models for each of them, assuming that there are exactly five individuals a,...,e who can love (vertical axis) and be loved (horizontal axis). A small red box at row x and column y indicates L(x,y).

 Fig. 1.2.1.1.,
Spacer[100],
Pane@Row[{
Column[{
Column[{"No column/row is empty",
Row[{
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True]},
{"b",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"c",Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True]},
{"d",Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],
Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True]},
{"e",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{Text["∀x ∃y L(y,x):"],SpanFromLeft},
{Text["1.Everyone is loved"],SpanFromLeft},
{Text["by someone.\n"],SpanFromLeft}
}],
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"b",Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"c",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],
Item["",Background->White,Frame->True]},
{"d",Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"e",Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{Text["∀x ∃y L(x,y):"],SpanFromLeft},
{Text["2.Everyone loves"],SpanFromLeft},
{Text["someone.\n"],SpanFromLeft}
}]
},"          "
]
},Center],
Column[{"The diagonal is nonempty/full",
Row[{
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"b",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"c",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True]},
{"d",Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"e",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{Text["∃x L(x,x):"],SpanFromLeft},
{Text["3.Someone loves"],SpanFromLeft},
{Text["him/herself.\n"],SpanFromLeft}
}],
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"b",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"c",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True]},
{"d",Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True]},
{"e",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True]},
{Text["∀x L(x,x):"],SpanFromLeft},
{Text["4.Everyone loves"],SpanFromLeft},
{Text["him/herself.\n"],SpanFromLeft}
}]
},"          "
]
},Center],
Column[{"One row/column is full:",
Row[{
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"b",Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],
Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{"c",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True]},
{"d",Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"e",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{Text["∃x ∀y L(x,y):"],SpanFromLeft},
{Text["5.Someone loves"],SpanFromLeft},
{Text["everyone.\n"],SpanFromLeft}
}],
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"b",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"c",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True]},
{"d",Item["",Background->White,Frame->True],
Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"e",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{Text["∃x ∀y L(y,x):"],SpanFromLeft},
{Text["6.Someone is loved"],SpanFromLeft},
{Text["by everone.\n"],SpanFromLeft}
}]
},"          "
]
},Center],
Column[{"The matrix is noneempty/full:",
Row[{
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"b",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"c",Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True]},
{"d",Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],
Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{"e",Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{Text["∃x ∃y L(x,y):"],SpanFromLeft},
{Text["7.Someone loves"],SpanFromLeft},
{Text["someone.\n"],SpanFromLeft},
{Text["∃x ∃y L(y,x):"],SpanFromLeft},
{Text["8.Someone is "],SpanFromLeft},
{Text["loved by someone.\n"],SpanFromLeft}
}],
Grid[{{Text[""],SpanFromLeft},
{"","a","b","c","d","e"},
{"a",Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{"b",Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],
Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{"c",Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],
Item["",Background->Red,Frame->True]},
{"d",Item["",Background->Red,Frame->True],
Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],
Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{"e",Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{Text["∀x ∀y L(x,y):"],SpanFromLeft},
{Text["9.Everyone loves"],SpanFromLeft},
{Text["everone.\n"],SpanFromLeft},
{Text["∀x ∀y L(y,x):"],SpanFromLeft},
{Text["10.Everyone is "],SpanFromLeft},
{Text["loved by everone.\n"],SpanFromLeft}
}]
},"          "
]
},Center]}
],
"                "
,
g1=Graph[{"10,9"\[DirectedEdge]4,"10,9"\[DirectedEdge]6,"10,9"\[DirectedEdge]5,5\[DirectedEdge]1,5\[DirectedEdge]3,4\[DirectedEdge]1,4\[DirectedEdge]2,4\[DirectedEdge]3,6\[DirectedEdge]3,6\[DirectedEdge]2,1\[DirectedEdge]"8,7",2\[DirectedEdge]"8,7",3\[DirectedEdge]"8,7"},VertexLabels->{
1->Placed["\InlineText",Tooltip],
2->Placed["∀x ∃y L(x,y)",Tooltip],
3->Placed["∃x L(x,x)",Tooltip],
4->Placed["∀x L(x,x)",Tooltip],
5->Placed["∃x ∀y L(x,y)",Tooltip],
6->Placed["∃x ∀y L(y,x)",Tooltip],
"8,7"->Placed[Column[{"∃x ∃y L(x,y)","∃x ∃y L(y,x)"}],Tooltip],
"10,9"->Placed[Column[{"∀x ∀y L(x,y)","∀x ∀y L(y,x)"}],Tooltip]
},EdgeStyle->Red,ImageSize->Large];
g2=Graph[{"10,9"\[DirectedEdge]4,"10,9"\[DirectedEdge]6,"10,9"\[DirectedEdge]5,5\[DirectedEdge]1,5\[DirectedEdge]3,4\[DirectedEdge]1,4\[DirectedEdge]2,4\[DirectedEdge]3,6\[DirectedEdge]3,6\[DirectedEdge]2,1\[DirectedEdge]"8,7",2\[DirectedEdge]"8,7",3\[DirectedEdge]"8,7"},VertexLabels->"Name",EdgeStyle->Red,ImageSize->Large];
Show[g2,g1,PlotLabel->Style["Hasse diagram of the implications",Bold,Large]]

}],
Spacer[100],
Pane@
Only for the formulas 9 and 10 is the model unique, all other formulas may be satisfied by several models.

The sequence of the quantifiers is important!

 So it is instructive to distinguish formulas ∀x ∃y L(y,x), and ∃x ∀y L(x,y). In both cases everyone is loved; but in the first case everyone (x) is loved by someone (y), in the second case everyone (y) is loved by just exactly one person (x).
 
 
 Fig. 1.2.1.2.: Truth Values of Quantifiers
,
Spacer[100],
data={{"Statement","True When","False When"},
{"∀x, P(x)","P(x) is true for every x.","There is an x for which P(x) is false."},
{"∃x, P(x)","There is an x for which P(x) is true.","P(x) is false for every x."}
};
Pane@makeTextTable[data],
Spacer[100],
data={{"Statement","True When","False When"},
{"∀x ∀y, P(x,y)","P(x,y) is true for every pair x,y.","There is at least one pair, x,y for which P(x,y) is false."},
{"∀x ∃y, P(x,y)","For every x, there is a y for which P(x,y) is true.","There is an x for which P(x,y) is false for every y."},
{"∃x ∀y, P(x,y)","There is an x for which P(x,y) is true for every y.","For every x, there is a y for which P(x,y) is false."},
{"∃x ∃y, P(x,y)","There is at least one pair x,y for which P(x,y) is true.","P(x,y) is false for every pair x,y."}
};
Pane@makeTextTable[data],
Spacer[100],
Pane@ Below are presented the laws of quantifiers:
 
 Fig. 1.2.1.3.
,
Spacer[100],
data={{"Laws of Quantifier Distribution:\n Let ϕ(x), ψ(x) be statements where x∈X\n and X is notempty set. Then:"},
{"∀x, ϕ(x) ⟹ ∃x, ϕ(x)"},
{"¬(∀x, ϕ(x)) ⟺ ∃x, ¬ϕ(x)"},
{"¬(∃x, ϕ(x)) ⟺ ∀x, ¬ϕ(x)"},
{"∀x, (ϕ(x) ∧ ψ(x)) ⟺ (∀x, ϕ(x) ∧ ∀x, ψ(x))"},

{"∃x, (ϕ(x) ∨ ψ(x)) ⟺ (∃x, ϕ(x) ∨ ∃x, ψ(x))"},
{"(∀x, ϕ(x) ∨ ∀x, ψ(x)) ⟹ ∀x, (ϕ(x) ∨ ψ(x))"},
{"∃x, (ϕ(x) ∧ ψ(x)) ⟹ (∃x, ϕ(x) ∧ ∃x, ψ(x))"}
};
Pane@makeTextTable[data],
Spacer[100],
Pane@  Fig. 1.2.1.4.
,data={{"Laws of Quantifier (In)Dependence:\n Let ϕ(x,y) be statements where x∈X \n and y∈Y, and X and Y are notempty sets.\n Then:"},
{"∀x, ∀y, ϕ(x, y) ⟺ ∀y, ∀x, ϕ(x, y)"},
{"∃x, ∃y, ϕ(x, y) ⟺ ∃y, ∃x, ϕ(x, y)"},
{"∃x, ∀y, ϕ(x, y) ⟹ ∀y, ∃x, ϕ(x, y)"}
};
Pane@makeTextTable[data],
Spacer[100],
Pane@1.2.2. Negation of statements involving variables,
Spacer[100],
Pane@Consider the statement  ∀ x∈U, p(x) . If this statement is true then its truth set is U. Its negation must be false and have truth set the empty set. Alternatively, if the statement is false (i.e. its truth set is a proper subset of U) then its negation has to be true. We claim that the negation is the statement ∃ x∈U, ¬p(x) . Clearly this is the negation if the original statement is true. If the original is false then there must have been some x for which p(x) was false. We conclude that the statement  ¬(∀ x, p(x)) is equivalent to ∃ x ¬p(x) . Similarly, ¬(∃ x, p(x)) is equivalent to ∀ x, ¬p(x) .

Fig. 1.2.2.1.: Truth Values of Negated Quantifiers,
Spacer[100],
data={{"Statement","True When","False When"},
{"¬(∃x, P(x)) ≡ ∀x, ¬P(x)","For every x, P(x) is false.","There is an x for which P(x) is true."},
{"¬(∀x, P(x)) ≡ ∃x, ¬P(x)","There is an x for which P(x) is false.","P(x) is true for every x."}
};
Pane@makeTextTable[data],
Spacer[100],
Pane@For statements involving more than one variable we have a similar situation. We give below a table of statements involving two quantifiers along with its negation.

Fig. 1.2.2.2.
,
Spacer[100],
makeTextTable[data0_]:=Module[{data},
(* FIXME data=Table[ToString[#,TraditionalForm]&/@(data0[[i]]),{i,1,Length[data0]}];*)

Text@Grid[data0,Background->{None,{Lighter[Yellow,.9],{White,Lighter[Blend[{Blue,Green}],.8]}}},Dividers->{{Darker[Gray,.6],{Lighter[Gray,.5]},Darker[Gray,.6]},{Darker[Gray,.6],Darker[Gray,.6],{False},Darker[Gray,.6]}},ItemSize->Automatic]

];data={{"Statement","Negation"},
{"\!\(\*FormBox[
RowBox[{"∀", 
RowBox[{"x", 
RowBox[{"∀", 
RowBox[{
StyleBox["y",
FontSlant->"Plain"], "    ", 
RowBox[{"p", 
StyleBox["(",
FontSlant->"Italic"], 
StyleBox[
RowBox[{"x", ",", "y"}],
FontSlant->"Italic"], 
StyleBox[")",
FontSlant->"Italic"]}]}]}]}]}],
TraditionalForm]\)","\!\(TraditionalForm\`∃ x \(∃ y\\ \\ \\ \(¬ p(x, y)\)\)\)"},
{"∀x ∃y   p(x,y)","\!\(TraditionalForm\`∃ x \(∀ y\\ \\ \\ \(¬ p(x, y)\)\)\)"},
{"∃x ∀y   p(x,y)","\!\(TraditionalForm\`∀ x \(∃ y\\ \\ \\ \(¬ p(x, y)\)\)\)"},
{"∃x ∃y   p(x,y)","∀x ∀y   ¬p(x,y)"}
};Pane@makeTextTable[data],
Spacer[100],
Pane@1.2.2.a. Negation,
Pane@We illustrate why the negation of ∀ x, ∀ y, p(x, y) is ∀ x, ∀ y, ¬p(x, y) using two sets X and Y, each having two elements. In the diagrams below, if p(x, y) is true we mark the square red and if it is false then we leave it white. There are of course 16 such diagrams.

Now consider the statement ∀ x, ∀ y, p(x, y). For this to be true we must have one of the following diagrams. This is because for at least one fixed x and every element of Y the statement is true. Thus there must be at least one red row. 

Fig. 1.2.2.a.1.,
Pane@Row[Framed/@{
Grid[{{Item["X",Background->White],Item["",Background->White,Frame->True],Item["",Background->Red,Frame->True]},{SpanFromAbove,Item["",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->White,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->Red,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All]
}],
Spacer[100],
Pane@It is false for the remaining nine diagrams shown below (since no row is all red).

Fig. 1.2.2.a.2.,
Spacer[100],
Pane@Row[Framed/@{
Grid[{{Item["X",Background->White],Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},{SpanFromAbove,Item["",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->Red,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->Red,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->White,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->Red,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->White,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->White,Frame->True],Item["",Background->Red,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All],

Grid[{{Item["X",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},{Item["",Background->White,Frame->False],Item[" ",Background->Red,Frame->True],Item["",Background->White,Frame->True]},
{SpanFromAbove,"Y",SpanFromLeft}
},ItemSize->All]
}],
Spacer[100], 

Pane@The situation is reversed for the statement ∀ x∈X, ∃ y∈Y ¬p(x,y). In this case, the statement is true if there is no completely red row and false when there is.





Practice by making similar statements below:
,
Spacer[100],
m2[],
Spacer[100],
Pane@1. Quantifiers and propositionals - examples,
Spacer[100],
m3[],
Spacer[100]
}],
"Method"->"Standalone"];

expr