The Logic Symbols font
by Scott Pakin


Valid characters in the Logic Symbols font:

&d0DSet operators&d@
N (N) -- Intersection
U (U) -- Union
G (G) -- Subset
H (H) -- Not a subset
C (C) -- Proper subset
D (D) -- Not a proper subset
= (=) -- Set equivalence
< (<) -- Set nonequivalence
' (') -- Set nonmembership

&d0DPredefined sets&d@
O (O) -- Empty set
P (P) -- Universal set

&d0DPropositional calculus&d@
^ (^) -- And
v (v) -- Or
~ (~) -- Not
> (>) or ) ()) -- Implies (if...then)
- (-) or # (#) -- Equivalence (if and only if)

&d0DPredicate calculus and miscellaneous&d@
A (A) -- For all
E (E) -- There exists
e (e) -- Membership
f (f) -- Nonmembership
: (:) -- Therefore



&d0DSample usages:&d@

p>q   p-q   pvq   p^q   ~p   p)q   p#q

P=Q   P<Q   PUQ   PNQ   PCQ   PDQ   PGQ   PHQ

P'=Q   O'=P   P''=O

Ax,yeA,(x>y)-(xv~y)
Ax,yeA,(x)y)#(xv~y)

(AP)(P<P>PCP)

Ep|(pfO)^(peP)

:P=Q



&d0DExample:&d@  Prove that set union distributes over set intersection.

In set notation, we must prove that for any A,B,CGP,
AU(BNC)=(AUB)N(AUC).  To do so, we can show that the left side
of the equation can be transformed into the right side of the equation.  By
the definitions of set union and intersection, we can rewrite the left side
of our initial equation as (xeA)v[(yeB)^(zeC)] Because v distributes
over ^, we can distribute the v over the ^ in the previous expression
to get [(xeA)v(yeB)]^[(xeA)v(zeC)].  Again using the definitions
of set union and intersection, we can rewrite the above as (AUB)N(AUC).
Because we have shown that, through the use of binary operators, AU(BNC)
can be transformed into (AUB)N(AUC), we can conclude that
AU(BNC)=(AUB)N(AUC), which is what we are trying to prove.