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:

F | G | F ⇒ 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+.