Sets — What They Are, What You Can Do With Them

What a set is

A set is just a collection of distinct things, with no order and no duplicates. {2, 4, 6} and {6, 2, 4, 2} are the same set — writing an element twice doesn't create two of it, and there's no "first" element. That's the entire idea. Everything else in this lesson is vocabulary for talking about sets precisely.

Membership: ∈ and ∉

x ∈ S means "x is an element of S" — this is called set membership. Its negation is x ∉ S — "x is not an element of S." In TLA+ you write these as \in and \notin:

2 \in {2, 4, 6}      \* true
3 \notin {2, 4, 6}   \* true

Subsets: ⊆

S ⊆ T ("S is a subset of T," the relation itself sometimes called inclusion) means every element of S is also an element of T. Note that S ⊆ S is always true — a set is a subset of itself. In TLA+, this is \subseteq:

{2, 4} \subseteq {2, 4, 6}   \* true
{2, 5} \subseteq {2, 4, 6}   \* false — 5 isn't in the right-hand set

You'll sometimes see ⊂ for proper subset — "a subset, but not equal to the whole thing." TLA+ has no separate operator for this; you just say what you mean directly: S \subseteq T /\ S # T (that /\ is "and" — logic is next chapter, but you already know enough to read this).

Combining sets: ∪, ∩, \

Three operators build new sets out of old ones:

{2, 4, 6} \union {4, 6, 8}      \* {2, 4, 6, 8} — everything from either set
{2, 4, 6} \intersect {4, 6, 8}  \* {4, 6}
{2, 4, 6} \ {4, 6, 8}           \* {2}

The empty set

The set with nothing in it is written {} in TLA+ (you'll also see it typeset as ∅ in books). {} ⊆ S is true for every set S — vacuously, every element of {} (there are none) is in S.

The power set: SUBSET

The power set of S, written 2^S, is the set of all subsets of S — including {} and S itself. If S has n elements, 2^S has 2ⁿ elements (hence the name). TLA+'s keyword for this is SUBSET:

SUBSET {1, 2} = {{}, {1}, {2}, {1, 2}}

This is the single most common point of confusion for newcomers: SUBSET computes the power set, it does not test whether something is a subset. That job belongs to \subseteq. Two completely different operators that happen to share a name in English.

Cartesian product: ×

S × T is the set of all ordered pairs <<s, t>> with s ∈ S and t ∈ T. TLA+ writes this S \X T, and tuples with double angle brackets:

{1, 2} \X {9} = {<<1, 9>>, <<2, 9>>}

Size: Cardinality

For a finite set, Cardinality(S) gives its number of elements. Unlike everything above, this isn't a bare TLA+ primitive — it lives in the FiniteSets standard module, so you need EXTENDS FiniteSets to use it.

What you'll do in this exercise

You'll write a handful of ASSUME statements — bare true/false claims about sets — and let TLC check every one of them. This is the first time you'll run TLC, and there's no state machine anywhere in sight: no VARIABLE, no Init, no Next. Every TLA+ file still needs the ---- MODULE Name ---- / ==== wrapper and an EXTENDS line to pull in library operators like Cardinality — treat that as required boilerplate for now. We'll unpack exactly what modules and EXTENDS really mean in Part 1.

If one of your ASSUME statements is false, TLC tells you immediately, pointing at the exact line — this is what makes it worth using as a calculator for checking your own reasoning about sets.