How to read formal logic notation — mapping ∀, ⇒, × to test code

Definition

Formal logic is a notation that writes sentences as symbols so that whether they are true or false can be determined mechanically from their form alone, rather than from their meaning.

The sentence “The button must be disabled for people who are not logged in” is read slightly differently by different people. Is it enough for the button not to appear, or may it appear but not be clickable? Writing the same content with symbols gives it one fixed reading.

This document explains symbols frequently used in specifications and proofs in three groups: set symbols that collect values, logical connectives that join true and false, and quantifiers that talk about “all” and “some.” Each symbol comes with code translated into TypeScript. Once you can read them as code, symbols are not difficult.

Why it matters

Testing ultimately asks, “Is this property preserved for these inputs?” When “these inputs” and “this property” are written in words, gaps appear in two places.

• The scope is vague. “Various screen sizes” does not say how many or where the boundaries are. Width = {320, ..., 3840} says there are 3,521 of them.
• The direction is vague. From “an editor can use it,” prose alone does not tell us whether it also means “only editors can use it.” Symbols distinguish ⇒ from ⇔, so they cannot be mixed up.

This matters especially when handing a specification to AI. A prose specification is easy to read in the direction that makes implementation convenient, while a symbolic specification leaves little room for that. Inputs accepted by a proof language such as Bend are ultimately these symbols translated into code.

How it works

Sets: a bag of collected values

A set is a collection of values without duplicates. In testing, use it when listing “all possible inputs.”

× (Cartesian product) is used most often when creating a test space.

The count grows by multiplication. Since ∣A × B∣ = ∣A∣ × ∣B∣, 2 × 3 makes 6 pairs. This is why the test space grows multiplicatively each time an axis is added.

const omega = widths.flatMap((width) =>
  auths.flatMap((auth) => roles.map((role) => ({ width, auth, role }))),
);

Notation such as {x ∈ A ∣ C(x)} is called set-builder notation. The vertical bar ∣ says “where to choose from” on the left and “under what condition” on the right. Its shape is exactly like filter.

Names such as Ω (omega) or P₁ are not special symbols; they are names given to sets. Subscripts are numbers. Ω₀ and Ω₁ mean the first space and the next version of that space.

Logical connectives: glue joining true and false

A proposition is a sentence determined to be either true or false. “768 is greater than 767” is a proposition; “Let’s make the button pretty” is not. Connectives join multiple propositions to make a new one.

Here are all combinations of true (T) and false (F). This is called a truth table.

The unfamiliar one is ⇒. P ⇒ Q is false in exactly one case: P is true and Q is false. If P is false, it is true whatever Q is.

It is easier to think of it as a promise. Suppose you say, “If it rains, I’ll bring an umbrella,” but it does not rain. Whether you brought one or not, you did not break the promise. There was no opportunity to break it. Thus in TypeScript it is !p || q.

This property creates vacuous truth in tests. If you check “logged-in users can edit” but have no logged-in input at all, every test passes. The condition was never true.

Be careful when reversing implication

Three propositions are derived from P ⇒ Q, but only one has the same meaning as the original.

The contrapositive of “not logged in means disabled” (¬Auth ⇒ ¬Enabled) is “if active, then logged in” (Enabled ⇒ Auth). They are exactly the same law, so use whichever is easier to test.

The inverse is also different. “Not logged in means disabled” does not imply “logged in means active.” A viewer can be logged in and still disabled. If you write only a prohibition law but mistake it for a guarantee in the reverse direction, an implementation that does nothing can pass the tests.

⇔ bundles two directions

≡ means that two expressions always have the same truth value. Thus one ⇔ contains two laws.

Expanding this one line gives:

• ⇒ direction: if active, all three conditions are true. Taking the contrapositive gives “if any one of the three is false, it is disabled,” from which prohibition laws L1–L3 follow.
• ⇐ direction: if all three conditions are true, it is active. This is obligation law L4.

Writing a specification with ⇔ pins down prohibitions and obligations together. Writing only ⇒ omits half of it.

Precedence

Without parentheses, group in the order ¬, ∧, ∨, ⇒, ⇔. It is like multiplication binding before addition.

When in doubt, add parentheses. No specification is wrong because it has too many parentheses.

Quantifiers: “all” and “some”

Connectives only speak about one input. To say “for every input,” you need quantifiers.

∀ resembles the A in All, and ∃ is an inverted E from Exists.

A function such as P(x) that takes an input and returns true or false is a predicate. In TypeScript, it is an (x) => boolean function.

A counterexample negates ∀

“Everyone is P” being false means there is at least one thing that is not P. That one is the counterexample.

This separates what tests and proofs can do.

• To show ∀ is true, check every case. If the space is finite and small, enumerate it; if it is infinite or large, a proof is needed.
• To show ∀ is false, one counterexample is enough. Finding that counterexample is what property-based testing tools do.

One thousand passing tests can be written like this.

If S is not all of Ω, ∀x ∈ Ω, P(x) remains unknown. The difference between passing tests and proof appears in one line of symbols.

∀ over an empty set is always true

This proposition is true whatever P is. There are no elements to check, so there is no element that violates it. In JavaScript, [].every(() => false) is also true. This is how an input space can accidentally become empty because filters contradict one another while the report says “all passed.” When checking ∀, also check its partner ∃: does an input satisfying the condition actually exist?

Changing quantifier order changes meaning

The left says “everyone has a mother.” The right says “there is one person who is everyone’s mother.” Swapping only two symbols creates a completely different claim.

The same applies to tests. “Every user has a role they can use” and “there is one role every user can use” are different requirements.

Function notation

Here π does not denote the circle constant; it is a name taken from “projection.” It is a function that decides “what to look at when judging equality.”

Applying it

Read long formulas from outside inward

defining-done-for-ai-code writes “perfect implementation” like this.

Peel off one layer at a time from the outside.

1. Perfect(I) ⇔ …: implementation I is perfect if and only if the right-hand side holds.
2. ∀x ∈ Ω: for every input x in space Ω
3. I(x): give x to the implementation
4. π(…): select the part of the result to inspect
5. P(x, …): it is true when passed to law P together with the input.

In code, this is one line.

const perfect = omega.every((x) => P(x, pi(I(x))));

Correspondence with Bend syntax

Proof language Bend 2 writes these symbols as code. The Bend guide explains that “a proposition is a type and a proof is a def of that type”; this correspondence is called the Curry–Howard correspondence.

The key point is that a proof of P ⇒ Q is a function. It is a promise: “Give me evidence for P and I will make evidence for Q.” Thus an assumption becomes a parameter, and when the goal reduces to the same shape as an assumption, returning that parameter completes the proof.

law wide_editor_is_enabled:
  for width: Nat
  for wide: {Nat.is_ge(width, 768n) == True{} : Bool}
  {E.enabled(True{}, E.Editor{}, width) == True{} : Bool}

def Laws.wide_editor_is_enabled(width, wide):
  wide

{==} proves equality by reflexivity: “after calculating both sides, they are identical.” The fact that ≠ is -> Empty follows the same principle. “Give me evidence that they are equal and I can produce the impossible” means “they are not equal.”

Steps for translating a specification into symbols

1. Write a set for each input axis, including range and unit, like Width = {320, …, 3840}.
2. Join the axes with × to make space Ω. If combinations must be removed, use {x ∈ Ω ∣ C(x)} and record the reason for C.
3. First write the law as ⇔. This reveals whether ⇒ alone is sufficient or the reverse direction is needed.
4. Prefix ∀x ∈ Ω, and in parallel check ∃x ∈ Ω (whether an input satisfying the law’s conditions actually exists).
5. Translate each symbol into TypeScript’s every, some, and filter, then run it over a small space.

Trade-offs

• Symbols are short and unambiguous, but they raise the barrier for first-time readers. In specification documents, put a plain-language explanation directly below the symbols.
• A precisely written symbolic specification can still be wrong. If you incorrectly write the boundary as 1000, that error is communicated precisely. Formalization removes ambiguity; it does not verify that the requirement itself is right.
• A ∀ over an infinite set cannot be checked by enumeration. You need a proof, and proofs cost much more than tests.

When not to use it

• Domains with multiple valid answers. Pinning layout details, wording, or recommendation order to one ⇔ line makes the specification break on normal changes.
• Prototypes where what to build is not yet decided. Writing the space and laws costs more than building.
• Leaving only symbols without a plain-language explanation when most teammates cannot read them. A specification nobody can review is not a specification.

Common mistakes

• Reading ⇒ as causation. P ⇒ Q does not mean “P causes Q”; it means there is no case where P is true and Q is false.
• Mistaking the inverse for the original. “Not logged in means disabled” does not imply “logged in means active.”
• Checking ∀ over an empty space. If conditions conflict, there are zero inputs and the test passes completely. Pair it with ∃.
• Mixing up ∈ and ⊆. ∈ means one element belongs to a set; ⊆ means an entire set is contained in another. 768 ∈ Width, {767, 768} ⊆ Width.
• Changing quantifier order carelessly. ∀∃ and ∃∀ are different claims.
• Reporting ∀x ∈ S as ∀x ∈ Ω. Tests have only checked the inputs in S.

Related concepts

• test-oracle: the law P written in symbols becomes the test oracle. It is about the source of “what is correct.”
• type-level-bva: how to choose boundary cases from space Ω.
• mutation-testing: deliberately make a specification violation, such as changing ≥ to >, and check whether the tests catch that counterexample.