Propositions and predicates
A proposition is a statement that is either true or false — 2 \in Evens is one, 4 + 4 is not (it's a number, not a claim). Logic is just
the rules for combining propositions into bigger ones.
A predicate is close but not quite the same thing: it's a statement with
a blank in it, like "x is even," that only becomes a proposition — only
becomes true or false — once you say what x is. Even(x) == x % 2 = 0 is
a predicate; Even(4) is the proposition you get by filling in the blank,
and it happens to be true. You'll see this distinction matter later:
TypeOK and Init are predicates about a state, true or false only once
you plug in a specific state.
And, or, not: ∧, ∨, ¬
| Symbol | Name | TLA+ | Meaning |
|---|---|---|---|
∧ |
conjunction | /\ |
and — true only if both sides are true |
∨ |
disjunction | \/ |
or — true if either side is true (or both) |
¬ |
negation | ~ |
not — flips true to false and back |
4 \in Evens /\ 4 \notin Odds \* true: both sides hold
3 \in Odds \/ 3 \in Evens \* true: at least one side holds
~(2 \in Odds) \* true: 2 is not odd
The gotcha: /\ and \/ don't mix without parentheses
This one catches everybody at least once. Chaining the same connective is
fine — A /\ B /\ C and A \/ B \/ C both parse exactly as you'd expect.
But mixing /\ and \/ in the same expression, without parentheses to
say which applies first, is a parse error:
A /\ B \/ C \* ✗ "Precedence conflict between ops \land and \lor"
TLA+ isn't guessing wrong here — it's refusing to guess at all. Rather than
silently picking a precedence you might not have meant (unlike most
languages, which quietly decide ∧ binds tighter than ∨ and hope you
knew that), it makes you say what you mean:
(A /\ B) \/ C \* ✓ says exactly what it means
A /\ (B \/ C) \* ✓ a different claim, also unambiguous
If you ever see "Precedence conflict" from TLC or the syntax checker, this is almost always why — go add the parentheses.
Implies and iff: ⇒, ⇔
| Symbol | Name | TLA+ | Meaning |
|---|---|---|---|
⇒ |
implication | => |
implies — if the left side is true, the right side must be too |
⇔ |
biconditional (or logical equivalence) | <=> |
iff ("if and only if") — both sides have the same truth value |
The one that surprises people: P ⇒ Q is true whenever P is false,
no matter what Q says. This is called vacuous truth — the implication
only makes a promise about what happens if P holds, so if P never
holds, there's nothing to break:
(100 \in Evens) => (1 = 2) \* true! 100 isn't even, so the claim is vacuous
Bounded quantifiers: ∀, ∃
These are how you say "for every element of a set" or "for some element of a set," without listing elements one by one.
∀x ∈ S : P(x) — the universal quantifier, read "for all x in
S, P(x) holds." In TLA+:
\A x \in Evens : x % 2 = 0 \* every element of Evens is even
∃x ∈ S : P(x) — the existential quantifier, read "there exists an
x in S such that P(x) holds." In TLA+:
\E x \in Odds : x > 5 \* at least one element of Odds is bigger than 5
This x \in S : ... shape — a bound variable, then a colon, then a
predicate about it — isn't unique to quantifiers. It's also how you write
set-builder notation: { x \in S : P(x) } means "the set of every x
in S for which P(x) holds." You'll see this exact shape again very soon,
when we get to invariants.
What you'll do in this exercise
More ASSUME statements, same as last chapter — still no state machine.
One of them is deliberately broken by the precedence gotcha above; the fix
is just parentheses, not a different fact.