Typing Expressions in Proof Designer

Proof Designer recognizes the following mathematical symbols. The symbols that are not on the keyboard can be entered either by clicking on the buttons in the symbol palette on the screen, or by using the keystrokes in the table below. (Note: In the table, “alt” refers to the alt key on a PC, and the option key on a Macintosh.)

Symbol	Meaning	How to Type It
∧	and	alt-A
∨	or	alt-O
→	if-then	alt-C (for conditional)
↔	if and only if	alt-B (for biconditional)
¬	not	alt-F (for false)
∀	for all	alt-shift-A
∃	there exists	alt-shift-E
!	unique (must follow ∃)
∈	element of	alt-M (for member of)
∉	not an element of	alt-shift-M
⊆	subset of	alt-S
⊈	not a subset of	alt-shift-S
=	equal to
≠	not equal to	alt-=
∩	intersection	alt-shift-I
∪	union	alt-shift-U
∖	set difference
△	symmetric difference	alt-D
×	cartesian product	alt-P
○	composition (of relations)	alt-shift-C
𝒫	power set	alt-shift-P
∅	empty set	alt-0 (alt-zero)
⁻¹	inverse (of a relation)	alt-1 (alt-one)
( , )	ordered pairs
{ \| }	set-builder notation
( ), [ ]	grouping

For the most part, these symbols are simply used in the usual way. Here's a quick summary of what that means.

There are two kinds of meaningful expressions in Proof Designer: statements and terms. A statement asserts that something is true, and a term is a name for an object. For example, A⊆B is a statement (it asserts that A is a subset of B), and A∩B is a term (it is a name for the intersection of A and B).

Terms

The simplest terms that Proof Designer recognizes are variables. You may use any letter (case matters) as a variable. You can also use a letter with a subscript between 0 and 999. (The subscript cannot be a variable; it must be a number.) To type a subscripted variable, just type the letter followed by the subscript; the digits will automatically be subscripted. Whenever it matters what kind of object a variable stands for, Proof Designer assumes that it stands for a set.

The symbol ∅ is also a term, and it stands for the null set—the set with no elements.

There are three ways you can use braces to form terms, illustrated by the following examples:

{a,b,c} is the set containing the three elements a, b, and c.
{x∈A|x⊆B} is the set of all elements of A that are subsets of B. Note that {x|x⊆B} is not allowed; you must specify a set from which the values of x are chosen. Proof Designer requires this in order to avoid Russell's Paradox.
{x∩B|x∈A} is the set of all sets of the form x∩B, where x is an element of A.

You can combine terms to form more complex terms using the symbols ∩, ∪, ∖, △, and 𝒫. These have the following meanings:

A∩B={x|x∈A and x∈B}
A∪B={x|x∈A or x∈B}
A∖B={x|x∈A and x∉B}
A△B=(A∖B)∪(B∖A)
𝒫(A)={x|x⊆A}

You can also use the symbol ∪ to form the union of a family of sets. If F is a set whose elements are all sets, then ∪F is the union of all of the sets in F. In other words:

∪F={x| For some A∈F, x∈A}

Similarly, you can use the symbol ∩ to form the intersection of a family of sets, but this can lead to problems if the family is empty. (For more on this, see the discussion of Russell's Paradox.) For this reason, Proof Designer requires that you explicitly include at least one set in any intersection. If U is a set and F is a family of sets, then you can write the intersection of U and all the elements of F as follows:

U∩∩F={x|x∈U and for all A∈F, x∈A}

You can also talk about ordered pairs. (a,b) is the ordered pair whose first coordinate is a and whose second coordinate is b. If A and B are sets, then A×B is the Cartesian product of A and B; i.e., it is the set of all ordered pairs (a,b) with a∈A and b∈B. Sets of ordered pairs are called relations, and you can use the symbols ○ and ⁻¹ to talk about compositions and inverses of relations:

R○S={(a,c)| For some b, (a,b)∈S and (b,c)∈R}
R⁻¹={(b,a)|(a,b)∈R}

Of course, you can combine all of these symbols to form complex expressions, using parentheses and brackets to group terms together if necessary. For example, the following are all terms:

[A∪(B×C)]∖𝒫(A∩B)
A△{x∈𝒫(B)|x∩C=∅}
∪{𝒫(x)|x∈F∪G}∩∩{x∈𝒫(F)|x⊈G}

Statements

The simplest statements that Proof Designer recognizes are those of the forms x∈y, x∉y, x=y, x≠y, x⊆y, and x⊈y. In all of these statements, the letters x and y can be replaced by any terms.

You can combine these basic statements to make more complex statements using the logical symbols ∧, ∨, →, ↔, and ¬. The symbols ∧, ∨, →, and ↔ must always occur between two statements, and the symbol ¬ must always occur before a statement. For example:

x∈A∧x∈B means that x∈A and x∈B.
x∈A∨x∈B means that x∈A or x∈B.
x∈A→x∈B means that if x∈A then x∈B.
x∈A↔x∈B means that x∈A if and only if x∈B.
¬x∈A means that it is not the case that x∈A.

The quantifier symbols ∀ and ∃ mean “for all” and “there exists”, respectively, and ∃! means “there exists a unique”. Each must be followed by a variable and then a statement. For example:

∀x(∅⊆x) means that for all x, ∅⊆x.
∃x(∅∈x) means that there exists some x such that ∅∈x.
∃!x(x⊆∅) means that there exists a unique x such that x⊆∅.

You can put a restriction on the range of possible values for the variable that comes after a quantifier as follows:

∀x∈A(x∈B) means the same thing as ∀x(x∈A→x∈B).
∃x∈A(x∈B) means the same thing as ∃x(x∈A∧x∈B).
∃!x∈A(x∈B) means the same thing as ∃!x(x∈A∧x∈B).

Parentheses ( ) and Brackets [ ]

You can use parentheses and brackets to eliminate ambiguity. When in doubt, put in extras—it can't do any harm. In the absence of parentheses or brackets, the following priority order determines the order in which expressions are combined:

Highest priority: ⁻¹
Next: All other unary operators, quantifiers, and ¬
Next: ∩, ∪, ∖, △, ○, and ×
Next: ∈, ⊆, =, ∉, ⊈, and ≠
Next: ∧ and ∨
Lowest priority: → and ↔