# 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 FALSETRUE 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 FALSETRUE, 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 TRUEFALSE. 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+.