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:

FGF ⇒ G
`TRUE``TRUE``TRUE`
`TRUE``FALSE``FALSE`
`FALSE``TRUE``TRUE`
`FALSE``FALSE``TRUE`

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+.