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)
-1 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).


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:

You can combine terms to form more complex terms using the symbols ∩, ∪, \, Δ, and ℘. These have the following meanings:

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:

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:

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 -1 to talk about compositions and inverses of relations:

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:


The simplest statements that Proof Designer recognizes are those of the forms x∈y, x∉y, x = y, xy, 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:

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:

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

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: