Basic Math for TLA+

At its most basic, TLA+ is a written description of what a system is supposed to do. More specifically, TLA+ is a specification language for formally defining the behavioural properties of a system.

TLA+ is based on temporal logic, which is built on top of first-order logic and set theory, and provides some conveniences for working with large specifications for complex systems. You can think of a TLA+ specification as mostly ordinary math and logic, glued together with temporal logic for parts requiring it.

Most of TLA+ is actually a language for writing math, and for turning mathematical specifications into an engineering tool for designing complex systems. As such, to work effectively with TLA+ requires first understanding a bit of the math behind it. But don’t worry, none of it is that complex.

Propositional Logic

TLA+ uses logic at its base — propositional logic to be more precise. In propositional logic, there are two base values TRUE and FALSE, and a handful of operators: ∧ (conjunction), ∨ (disjunction), ¬ (negation), ⇒ (implication), and ≡ (equivalence). These operators should already be fairly familiar to most programmers but are defined here, just in case:

∧ (conjunction) : F ∧ G equals TRUE iff both F and G equal TRUE

∨ (disjunction) : F ∨ G equals TRUE iff both F or G (or both) equal TRUE

¬ (negation)

¬F equals TRUE iff F equals FALSE

⇒ (implication)

F ⇒ G equals TRUE iff F equals FALSE or G equals TRUE (or both).

≡ (equivalence)

F ≡ G equals TRUE iff F and G both equal TRUE or both equal FALSE.

Implication (F ⇒ G) can be difficult to understand given the definition alone. In more detail, it means F implies G, but why would FALSE ⇒ TRUE evaluate to TRUE? By using some concrete numbers we can arrange an expression like (n > 3) ⇒ (n 1), which, if n = 4, will be TRUE ⇒ TRUE, which is a true statement. If n = 2, we get FALSE ⇒ TRUE, which is a true statement as well. And if n = 0, we get FALSE ⇒ FALSE, which is also a true statement. In fact, the only case where ⇒ evaluates to FALSE is if you have a logically FALSE statement, like TRUE ⇒ FALSE. As a truth table, we can prescribe ⇒ as follows:

If you are ever in doubt about how to evaluate a statement in propositional logic, you can always write out truth tables for each element and evaluate them by hand.

Set Theory

Set theory is the foundation of regular math, and TLA+ leverages this foundation for writing specifications. Sets can have a finite or infinite number of elements, and each set is completely determined by the elements in the set — sets cannot contain duplicates. Sets contain a few operations of interest to TLA+:

∈ (set membership)

x ∈ S is TRUE if the element x is in the set S.

∩ (intersection)

S ∩ T is the set of all elements in both S and T.

∪ (union)

S ∪ T is the set of all elements in S or T (or both).

∖ (difference)

S ∖ T is the set of all elements in S that are not in T.

⊆ (subset)

S ⊆ T evaluates to TRUE iff every element of S is an element of T.

Predicate Logic

Whereas propositional logic provides logical operators for individual elements, predicate logic provides operators for sets. Particularly:

∀ (universal quantification)

∀ implies that a statement holds for all elements in a set. It is usually read as “for all”.

∃ (existential quantification)

∃ implies that there exists an element in a set, for which a statement holds. It is usually read as “there exists”.

The formula ∀ x ∈ S : F asserts that formula F is TRUE for every element x in the set S. The formula ∃ x ∈ S : F asserts that formula F is TRUE for at least one element x in S.

And That’s All — For Now

These are the basics required to read and write TLA+. I will use these basics in future articles to show on TLA+.