Expressions, unknowns and rules

Kojo and Ama are shopping at the market in Kumasi, in Ghana. They buy a bag for 2 cedis and 3 bottles of water at 4 cedis each. Kojo types into his small calculator:

His calculator says 20. Ama types exactly the same keys into the calculator on her phone. It says 14.

Which one is right? The shopkeeper knows: the bag costs 2 cedis, and the three bottles cost $3 \times 4 = 12$ cedis, so the total is $2 + 12 = 14$ cedis. Kojo's calculator worked from left to right as he typed, $2 + 3 = 5$, then $5 \times 4 = 20$ — as if he had bought 5 bottles!

Mathematicians all over the world have agreed on a rule for reading an expression like $2 + 3 \times 4$, so that everybody gets the same answer. In this lesson you will learn that rule, and then use it to find numbers that are hiding.

An expression like $3 \times 4 + 2$ is a name for a number. It names 14. The number 14 has many other names: $10 + 4$, $2 \times 7$, $20 - 6$, $(3 + 4) \times 2$.

Brackets say "work this out first". In $(2 + 3) \times 4$, we add first: $5 \times 4 = 20$. In $2 + (3 \times 4)$, we multiply first: $2 + 12 = 14$.

What if there are no brackets? Think about how we talk. "Three bags of 4 oranges, and 2 more oranges" is $3 \times 4 + 2$. It would be a nuisance to write brackets every time: $(3 \times 4) + 2$. So everybody agrees: multiplication and division are done before addition and subtraction, unless brackets say otherwise. Then $3 \times 4 + 2$ and $2 + 3 \times 4$ both mean "some groups, plus some more" — just what we usually want.

Sometimes a number is hidden, and we only know something about it:

"Three times some number makes 24." Which number is in the box? You may know straight away: 8. In this lesson you will learn a way that works even when the numbers are big — by undoing what was done to the hidden number.

The same reasoning shows that $3 \times \square = 24$ has exactly one answer: if $3 \times \square = 24$, divide both sides by 3. Dividing by 3 undoes multiplying by 3, so $\square = 24 \div 3 = 8$; and $3 \times 8 = 24$.

When there is no answer. Not every equation has a whole-number answer.

• $3 \times \square = 25$: we know $3 \times 8 = 24$ (too small) and $3 \times 9 = 27$ (too big), and the bigger the number in the box, the bigger $3 \times \square$ gets. So no whole number works. (A fraction does: $25 \div 3 = 8\tfrac{1}{3}$. You can meet it in Fractions and decimals.)
• $0 \times \square = 5$: zero times any number is 0, never 5. No number works at all.
• $0 \times \square = 0$: this is true for every number, so it does not tell us what is in the box.

That is why "multiplying is undone by dividing" needs the number to be non-zero. Multiplying by 0 sends 3 to 0 and 7 to 0 — and once you only see the 0, nothing can tell you whether it came from 3 or from 7. It cannot be undone.

An equation is like a balance: the two sides weigh the same. Each box on the scale holds the same unknown number of weights. Do the same thing to both sides — take 1 away from both, or divide both into equal shares — and the scale stays level. When one box is left alone, you have found the unknown.

What to notice:

• In the second scale, try dividing by 3 first. The scale refuses: 20 weights cannot be split into 3 equal shares. Undoing the "+ 2" first makes the division work — the last step is undone first.
• The record beside the scale is a list of equations, each one true. That list is your working.

Rules make growing patterns, too. Here each step $n$ has $2 \times n + 1$ tiles. Predict the number of tiles in step 10 before you reveal the rule.

Gideon only plays with statements that are exactly true or exactly false. Decide, and give a reason.

1. "$2 + 3 \times 4 = 20$." — False. Multiplication comes first: $2 + 12 = 14$.
2. "$(2 + 3) \times 4 = 20$." — True. The brackets are worked out first.
3. "The only number that makes $\square + 17 = 40$ true is 23." — True. Subtracting 17 from both sides shows it must be 23, and $23 + 17 = 40$.
4. "$3 \times \square = 25$ has a whole-number answer." — False. $3 \times 8 = 24$ and $3 \times 9 = 27$; 25 is in between.
5. "$24 = 3 \times \square$ is not a proper equation, because the answer must come after the equals sign." — False! "=" means "has the same value as". The equation is fine, and $\square = 8$.

/-- Without brackets, multiplication comes before addition: `2 + 3 * 4` is `2 + 12 = 14`.
Brackets change the grouping: `(2 + 3) * 4` is `5 * 4 = 20`. Lean follows the same convention
as the lesson. -/
theorem order_of_operations : 2 + 3 * 4 = 14 ∧ (2 + 3) * 4 = 20 := by
  decide

/-- Operations of the same kind are done from left to right: `18 / 3 * 2` is `6 * 2 = 12`
(not `18 / 6 = 3`), and `10 - 4 - 3` is `6 - 3 = 3` (not `10 - 1 = 9`). And `20 - 8 / 4` is
`20 - 2 = 18`, because division comes before subtraction. -/
theorem left_to_right : 18 / 3 * 2 = 12 ∧ 10 - 4 - 3 = 3 ∧ 20 - 8 / 4 = 18 := by
  decide

/-- Subtracting `b` undoes adding `b`: whatever number `n` you start with, add `b` and then take
`b` away, and you are back at `n`. This is core Lean's `Nat.add_sub_cancel`. -/
theorem sub_undoes_add (n b : Nat) : n + b - b = n :=
  Nat.add_sub_cancel n b

/-- Dividing by `a` undoes multiplying by `a`, as long as `a` is not 0. This is core Lean's
`Nat.mul_div_cancel_left`. -/
theorem div_undoes_mul (n a : Nat) (ha : 0 < a) : a * n / a = n :=
  Nat.mul_div_cancel_left n ha

/-- Multiplying by 0 **cannot** be undone: it sends 3 and 7 (and every other number) to the same
answer, 0, so nothing can tell us afterwards which number we started with. -/
theorem zero_cannot_be_undone : 0 * 3 = 0 * 7 ∧ 3 ≠ 7 := by
  decide

/-- **□ + 17 = 40 exactly when □ = 23.** If □ + 17 = 40, then taking 17 away from both sides
gives □ = 40 − 17 = 23 — so 23 is the only possible answer. And 23 really works. -/
theorem add_unknown (x : Nat) : x + 17 = 40 ↔ x = 23 := by
  constructor
  · intro h
    calc x = x + 17 - 17 := (Nat.add_sub_cancel x 17).symm
      _ = 40 - 17 := by rw [h]
      _ = 23 := by decide
  · intro h
    rw [h]

/-- The same reasoning for **any** numbers: when `b ≤ c`, the equation □ + b = c has exactly one
whole-number answer, □ = c − b. -/
theorem add_solution (b c x : Nat) (h : b ≤ c) : x + b = c ↔ x = c - b := by
  omega

/-- **3 × □ = 24 exactly when □ = 8.** If 3 × □ = 24, dividing both sides by 3 gives
□ = 24 ÷ 3 = 8. And 8 really works. -/
theorem mul_unknown (x : Nat) : 3 * x = 24 ↔ x = 8 := by
  constructor
  · intro h
    calc x = 3 * x / 3 := (Nat.mul_div_cancel_left x (by decide)).symm
      _ = 24 / 3 := by rw [h]
      _ = 8 := by decide
  · intro h
    rw [h]

/-- The equals sign means "has the same value as", so an equation can be written either way
round: 24 = 3 × □ is the same equation as 3 × □ = 24, with the same answer. -/
theorem unknown_on_left (x : Nat) : 24 = 3 * x ↔ x = 8 := by
  constructor
  · intro h
    exact (mul_unknown x).mp h.symm
  · intro h
    exact ((mul_unknown x).mpr h).symm

/-- **Two steps.** "Multiply by 3, then add 1" gives 22 exactly when the number was 7. To find
it, undo the steps in reverse order: take away 1, then divide by 3. -/
theorem think_of_a_number (x : Nat) : 3 * x + 1 = 22 ↔ x = 7 := by
  constructor
  · intro h
    calc x = (3 * x + 1 - 1) / 3 := by
          rw [Nat.add_sub_cancel, Nat.mul_div_cancel_left x (by decide)]
      _ = (22 - 1) / 3 := by rw [h]
      _ = 7 := by decide
  · intro h
    rw [h]

/-- Some equations have **no** whole-number answer: 3 × □ = 25 has none, because 25 is not a
multiple of 3 (`3 × 8 = 24` is too small and `3 × 9 = 27` too big). The answer is the fraction
25/3, which lives outside the whole numbers. -/
theorem no_whole_answer : ¬ ∃ x : Nat, 3 * x = 25 := by
  omega

/-- Why "multiplying by a **non-zero** number" matters: 0 × □ = 5 has no answer at all, and
0 × □ = 0 is true for every number, so it does not pin down □. -/
theorem zero_times_unknown : (∀ x : Nat, 0 * x ≠ 5) ∧ (∀ x : Nat, 0 * x = 0) :=
  ⟨fun x => by rw [Nat.zero_mul]; decide, fun x => Nat.zero_mul x⟩

/-- The rule "double, then add 1", written as an expression in `n`: `2 * n + 1`. -/
def doubleAddOne (n : Nat) : Nat := 2 * n + 1

/-- Completing the table for the rule: the inputs 1, 2, 3 and 10 give 3, 5, 7 and 21. -/
theorem doubleAddOne_table : [1, 2, 3, 10].map doubleAddOne = [3, 5, 7, 21] := by
  decide

/-- Working backwards: the rule gives 15 only for the input 7 (undo: take away 1, then
halve). -/
theorem doubleAddOne_backwards (n : Nat) : doubleAddOne n = 15 ↔ n = 7 := by
  unfold doubleAddOne
  omega

/-- The rule found from the table 1 → 4, 2 → 7, 3 → 10, 4 → 13: "multiply by 3, then add 1". -/
def threeNPlusOne (n : Nat) : Nat := 3 * n + 1

/-- The rule fits every row of the table. -/
theorem threeNPlusOne_table : [1, 2, 3, 4].map threeNPlusOne = [4, 7, 10, 13] := by
  decide

/-- Why the multiplier is 3: for **every** input, going up by 1 makes the output go up by 3. -/
theorem threeNPlusOne_step (n : Nat) : threeNPlusOne (n + 1) = threeNPlusOne n + 3 := by
  unfold threeNPlusOne
  omega

"""Two ways to read an expression: left to right, or by the convention.

A simple calculator works from left to right as you type, so it reads
2 + 3 x 4 as (2 + 3) x 4 = 20. The convention used in mathematics (and by
scientific calculators and programming languages) does multiplication and
division before addition and subtraction, giving 2 + 12 = 14. The program
evaluates some expressions both ways, then checks every expression
'a op b op c' with digits 1 to 9 and the four operations, and reports for
each pair of operations how often the two readings agree. Division is exact
(fractions), so nothing is rounded.
"""

import textwrap
from fractions import Fraction

OPS = {
    "+": lambda x, y: x + y,
    "-": lambda x, y: x - y,
    "x": lambda x, y: x * y,
    "/": lambda x, y: x / y,
}

def tokens(text):
    """Split '2 + 3 x 4' into numbers (as Fractions) and symbols."""
    return [Fraction(t) if t.isdigit() else t for t in text.split()]

def left_to_right(toks):
    """Work strictly from left to right, as a simple calculator does."""
    value = toks[0]
    for i in range(1, len(toks), 2):
        value = OPS[toks[i]](value, toks[i + 1])
    return value

def by_convention(toks):
    """Brackets first, then x and /, then + and -, each left to right."""
    pos = 0

    def factor():
        nonlocal pos
        if toks[pos] == "(":
            pos += 1
            value = expression()
            pos += 1  # skip ")"
            return value
        pos += 1
        return toks[pos - 1]

    def term():
        nonlocal pos
        value = factor()
        while pos < len(toks) and toks[pos] in ("x", "/"):
            op = toks[pos]
            pos += 1
            value = OPS[op](value, factor())
        return value

    def expression():
        nonlocal pos
        value = term()
        while pos < len(toks) and toks[pos] in ("+", "-"):
            op = toks[pos]
            pos += 1
            value = OPS[op](value, term())
        return value

    return expression()

    """How many of the 729 'a op1 b op2 c' read the same both ways."""
def agreement(op1, op2):
    """How many of the 729 expressions 'a op1 b op2 c' read the same both ways."""
    same = 0
    for a in range(1, 10):
        for b in range(1, 10):
            for c in range(1, 10):
                toks = [Fraction(a), op1, Fraction(b), op2, Fraction(c)]
                same += left_to_right(toks) == by_convention(toks)
    return same

def main():
    print("Expression        left to right   by the convention")
    for text in ["2 + 3 x 4", "20 - 8 / 4", "18 / 3 x 2", "10 - 4 - 3",
                 "3 x 4 + 2"]:
        toks = tokens(text)
        print(f"{text:<17} {str(left_to_right(toks)):>13}"
              f"   {str(by_convention(toks)):>17}")
    print("(2 + 3) x 4       brackets first: "
          f"{by_convention(tokens('( 2 + 3 ) x 4'))}")
    print()
    print("Every 'a op1 b op2 c' with digits 1-9: out of 729, how many")
    print("give the same answer read both ways?")
    print("op1 \\ op2 " + "".join(f"{op2:>7}" for op2 in OPS))
    for op1 in OPS:
        row = "".join(f"{agreement(op1, op2):>7}" for op2 in OPS)
        print(f"   {op1}      {row}")
    print("The readings can only differ when + or - comes before x or /.")
    print()
    print(textwrap.fill(
        "Epistemic status: exact (fractions, no rounding) and exhaustive for "
        "the 11664 expressions with three digits from 1 to 9. It shows when "
        "the convention matters; it does not show that the convention is "
        "'true'. The order of operations is an agreement, chosen so that "
        "expressions like 3 x 4 + 2 need no brackets.",
        width=78,
    ))

if __name__ == "__main__":
    main()

The two calculators always agree except when $+$ or $-$ comes before $\times$ or $\div$. Even then they agree in 81 of the 729 cases — exactly when the last number is 1, because multiplying or dividing by 1 changes nothing.

"""Which rule made this table? Searching input-output rules.

A table of inputs and outputs is evidence about a rule. The program tries
every rule of the form 'multiply by a, then add b' (a x n + b) with a and b
from 0 to 10 and lists those that fit the first rows of a table. One row
fits several rules; two rows pin down one rule of this kind - but a rule of
a different kind (n x n + 3) also fits those two rows, and only a third row
tells them apart. Finally it works backwards: which input gives a chosen
output, found by undoing the rule's steps in reverse order and checked by
running the rule forwards.
"""

import textwrap

TABLE = [(1, 4), (2, 7), (3, 10), (4, 13)]

def fits(rule, rows):
    """Does the rule give the right output for every row (input, output)?"""
    return all(rule(n) == out for n, out in rows)

def linear_rules_that_fit(rows, largest=10):
    """All (a, b) with 0 <= a, b <= largest such that a x n + b fits."""
    return [(a, b)
            for a in range(largest + 1)
            for b in range(largest + 1)
            if fits(lambda n, a=a, b=b: a * n + b, rows)]

def square_plus_three(n):
    """A rule of a different kind: n x n + 3."""
    return n * n + 3

def undo_three_n_plus_one(output):
    """Undo 'multiply by 3, then add 1' in reverse: take 1, then divide by 3.

    Returns None when there is no whole-number input."""
    if output < 1 or (output - 1) % 3 != 0:
        return None
    return (output - 1) // 3

def main():
    print("The table: " + ", ".join(f"{n} -> {out}" for n, out in TABLE))
    print("Rules 'a x n + b' (a, b from 0 to 10) that fit the first rows:")
    for k in range(1, len(TABLE) + 1):
        found = linear_rules_that_fit(TABLE[:k])
        rules = ", ".join(f"{a} x n + {b}" for a, b in found)
        rows = "row: " if k == 1 else "rows:"
        print(f"  {k} {rows} {rules}")
    print()
    print("A different kind of rule: n x n + 3")
    for k in (2, 3):
        print(f"  fits the first {k} rows:"
              f" {fits(square_plus_three, TABLE[:k])}")
    print("  (3 x 3 + 3 = 12, but the table says 3 -> 10.)")
    print()
    print("Working backwards from outputs of 3 x n + 1:")
    for output in (22, 31, 100, 24):
        n = undo_three_n_plus_one(output)
        if n is None:
            print(f"  output {output}: no whole-number input")
        else:
            print(f"  output {output}: input {n}"
                  f"  (check: 3 x {n} + 1 = {3 * n + 1})")
    print()
    print(textwrap.fill(
        "Epistemic status: exact and exhaustive, but only for rules of the "
        "form a x n + b with a and b from 0 to 10. A table with a few rows "
        "never proves which rule made it - other kinds of rules can fit the "
        "same rows. Knowing the rule, the backward answers are certain: each "
        "is checked by running the rule forwards.",
        width=78,
    ))

if __name__ == "__main__":
    main()

One row of the table fits five different rules. Two rows leave just one rule of this kind, $3 \times n + 1$. But a rule of a different kind, $n \times n + 3$, also fits the first two rows: $1 \times 1 + 3 = 4$ and $2 \times 2 + 3 = 7$! Only the third row tells them apart. A computer search like this is exact for the rules it tries, but a table with a few rows can never prove which rule made it.

Work out brackets first, then multiplication and division, then addition and subtraction. Always check an unknown by putting it back into the equation. You can ask for a hint whenever you like.

For an equation with an unknown, we can collect all the numbers that make it true into a set, called its solution set:

• $\square + 17 = 40$ has the solution set $\{23\}$: exactly one answer.
• $3 \times \square = 25$ has no whole-number answer: its solution set (among whole numbers) is the empty set $\{\}$.
• $0 \times \square = 0$ is true for every whole number: its solution set is the set of all whole numbers.

"Solve the equation" means "find the solution set" — and the two parts of our proof show exactly that the solution set of $\square + 17 = 40$ is $\{23\}$: nothing else is in it, and 23 is.

"Multiply by 3, then add 1" is a chain of two actions, one after the other. Undoing it means undoing the steps in the reverse order: first "subtract 1", then "divide by 3" — just as you take off your shoes before your socks. You can explore chains of actions, and why undoing goes backwards, in One thing after another.

• Egypt. The Rhind Mathematical Papyrus, copied by the scribe Ahmes around 1550 BCE from an older text, contains problems with an unknown quantity, called aha ("heap"). Problem 24 asks for a quantity which, together with one seventh of itself, makes 19. The scribe solved it by "false position": try 7 (then 7 plus its seventh is 8), and then scale up, giving $16\tfrac{5}{8}$.
• China. The Nine Chapters on the Mathematical Art, compiled about two thousand years ago, solves problems with several unknown quantities at once, using counting rods laid out on a board.
• India. Indian mathematicians, from Brahmagupta in the 7th century onwards, named unknown quantities with words, such as yāvat-tāvat ("as much as"), and used the names of colours — "black", "blue", "yellow" — when there were several unknowns at once.
• Baghdad. Around 820 CE, Muḥammad ibn Mūsā al-Khwārizmī wrote a book on solving equations. Its title contains the word al-jabr, "restoring": moving a quantity that is taken away on one side of an equation to the other side. That word became our word algebra.
• The equals sign. In 1557 the Welsh mathematician Robert Recorde introduced "=" in The Whetstone of Witte, choosing two parallel lines because "no two things can be more equal".
• Letters. In 1591 François Viète in France used letters for unknown and known numbers; in 1637 René Descartes used $x$, $y$ and $z$ for unknowns, as we still do.
• The order of operations grew up gradually as mathematicians wrote more and more algebra; it has no single inventor. Today it is taught, with small differences in the names (such as BODMAS, BIDMAS and PEMDAS), all over the world.

• Gay Robins and Charles Shute, The Rhind Mathematical Papyrus: An Ancient Egyptian Text (1987) — the papyrus, with its aha problems, explained.
• Victor J. Katz, A History of Mathematics: An Introduction (1993; later editions) — the history of algebra in Egypt, Mesopotamia, China, India and the Islamic world.
• Liping Ma, Knowing and Teaching Elementary Mathematics (1999) — how deep understanding of arithmetic, including inverse operations, prepares children for algebra.
• George Pólya, How to Solve It (1945) — including "working backwards", the strategy behind undoing steps in reverse order.