1. The order of choices
A statement with several quantifiers makes its choices in a fixed order. Swapping two quantifiers can change what the statement requires, even though every symbol stays the same. Definograph's Choices view lists the choices in order and says which earlier choices each one may use.
Two statements
These two statements about real numbers differ only in the order of ∀ x and ∃ y. They are the entries For every x, some y and Some y, for every x in Definograph's Statement menu.
∀ x : ℝ, ∃ y : ℝ, x < y
∃ y : ℝ, ∀ x : ℝ, x < y
∀ means "for every" and ∃ means "there exists". x : ℝ introduces a variable x that ranges over the real numbers. The comma separates a quantifier from the part of the statement it governs.
The first says: for every real x there is a real y with x < y. It is true: take y = x + 1.
The second says: there is a real y such that x < y for every real x. It is false: such a y would have to be larger than itself.
What Definograph shows
This is the Choices view of the first statement.
Recorded Definograph output · Lean 4.28.0 ·
Lean statement, as entered in Definograph
∀ x : ℝ, ∃ y : ℝ, x < y
A witness can use earlier choices in its scope. It cannot depend on a variable chosen later.
Scope and dependency- 1Arbitrary choice
An arbitrary element of this type. A displayed sample represents one choice, never every element.
- 2Candidate witness
Choose a witness using only earlier choices available in this scope. Its existence remains an obligation.
May depend on
Steps follow the statement’s reading order. Only the listed dependencies belong to the same scope; choices in separate logical branches are not combined.
x < y.Read it from top to bottom.
- Each numbered step is one choice, in the order the statement makes it.
- Step 1, marked ∀, is an arbitrary choice: the rest of the statement must hold whatever value x takes.
- Step 2, marked ∃, is a candidate witness. The statement asks for a suitable y, but the view does not supply one: "Its existence remains an obligation."
- May depend on means that a choice of y may use the value of x, because y is chosen after x. The gray a is a kind badge, not part of the statement.
Now the second statement.
Recorded Definograph output · Lean 4.28.0 ·
Lean statement, as entered in Definograph
∃ y : ℝ, ∀ x : ℝ, x < y
A witness can use earlier choices in its scope. It cannot depend on a variable chosen later.
Scope and dependency- 1Candidate witness
Choose a witness using only earlier choices available in this scope. Its existence remains an obligation.
Chosen without earlier values. Later choices cannot change this witness.
- 2Arbitrary choice
An arbitrary element of this type. A displayed sample represents one choice, never every element.
Earlier choices in this scope
Steps follow the statement’s reading order. Only the listed dependencies belong to the same scope; choices in separate logical branches are not combined.
x < y.- y is now step 1, and the view adds: "Later choices cannot change this witness."
- x is step 2. Every value of x must be handled, and y is already fixed when x is chosen.
Read the difference
| Statement | Order in the view | What the statement requires |
|---|---|---|
∀ x : ℝ, ∃ y : ℝ, x < y | x, then y. y may depend on x. | For each x, some y larger than that x. |
∃ y : ℝ, ∀ x : ℝ, x < y | y, then x. y is fixed first. | One y larger than every x. |
"May depend" permits dependence; it does not demand it. A statement of the first shape can still have one y that works for every x. Whether it does depends on the condition, not on the order of the choices.
What the view does not tell you
- Whether a witness exists. The two views have the same kind of steps, yet one statement is true and the other is false. Definograph reads statements; it does not prove them.
- The condition. The Choices view leaves out
x < y. Lesson 2 shows views that include it. - Which witness. "Candidate witness" names what the statement asks for, not a value.
- Anything from the letters. The view follows each variable by its place in the statement, not by its name. Renaming x and y changes the labels and nothing else.
Find the view in Definograph
With Definograph running on your computer (see Try it yourself in Setup), choose For every x, some y from the Statement menu. Definograph opens with its Visual sequence. Choose Explore a sample: the other representations appear as tabs. For this statement Choices, the view shown above, opens first. The second statement is Some y, for every x.
The Visual sequence says the same thing in its list of variables: under y, it notes whether y may use x.
Exercises
Exercise 1.1. Using the first view, choose y when x = 3 and when x = −10. Then give one rule that works for every x.
Hint
The view allows the choice of y to use x.
Answer
For example, y = 4 and y = −9. The rule y = x + 1 works for every x. It uses x, which the order of the choices allows.
The two values only illustrate the rule. It covers every x because x < x + 1 holds for an arbitrary x.
Exercise 1.2. Use the order in the second view to explain why the second statement is false.
Hint
x is chosen after y, and x can be any real number.
Answer
Whatever y is fixed at step 1, step 2 must allow every real number x, including x = y. For that x the condition reads y < y, which is false. So no y meets the requirement.
This rules out every candidate at once. It is stronger than trying a few values of y and finding none that works.
Exercise 1.3. This statement is Definograph's example Read ε–δ continuity in pieces:
∀ ε : ℝ, 0 < ε →
∃ δ : ℝ, 0 < δ ∧
∀ x : ℝ, |x| < δ → |x * x| < ε
Between two conditions, → means "implies" and ∧ means "and". |x| is the absolute value of x. Here is its Choices view:
Recorded Definograph output · Rendered · from saved results · Adapts to page theme · Native capture date unavailable · Dates in UTC · Saved input: Lean 4.28.0 · Lean was not rerun.
Source
Lean statement, as entered in Definograph
∀ ε : ℝ, 0 < ε →
∃ δ : ℝ, 0 < δ ∧
∀ x : ℝ, |x| < δ → |x * x| < ε
A witness can use earlier choices in its scope. It cannot depend on a variable chosen later.
Scope and dependency- 1Arbitrary choice
An arbitrary element of this type. A displayed sample represents one choice, never every element.
- 2AssumptionConditional on the premiseUnder 1 assumption
A local hypothesis; it is available only within this scope.
Earlier choices in this scope - 3Candidate witnessConditional on the premiseUnder 1 assumption
Choose a witness using only earlier choices available in this scope. Its existence remains an obligation.
May depend on - 4Arbitrary choiceConditional on the premiseUnder 1 assumption
An arbitrary element of this type. A displayed sample represents one choice, never every element.
Earlier choices in this scope - 5AssumptionConditional on the premiseUnder 2 assumptions
A local hypothesis; it is available only within this scope.
Earlier choices in this scope
Steps follow the statement’s reading order. Only the listed dependencies belong to the same scope; choices in separate logical branches are not combined.
ε, δ and x and the two assumptions in reading order, with the earlier choices each one may depend on. The view leaves out the conditions 0 < δ and |x * x| < ε.The steps marked ⇒ are the two assumptions, 0 < ε and |x| < δ. The statement gives them no names, so the view shows each under the name Lean gives it, a. This a is a name, not the gray kind badge before ε, δ and x. A tag such as Under 1 assumption counts the assumptions in force at that step; on an assumption's own step the count includes that assumption.
Which choices may δ depend on? May δ depend on x? What would the statement say if it could?
Hint
Compare the step numbers of δ and x, and read the list under δ.
Answer
δ may depend on ε: the view lists ε under May depend on. It may not depend on x, which is chosen later, at step 4. So a single δ must work for every x with |x| < δ.
If δ could depend on x, the statement would say almost nothing. For x ≠ 0 you could take δ = |x|. Then |x| < δ is false, so the implication holds for that x whatever the value of |x * x|.
Exercise 1.4. In ∀ x : ℝ, ∃ y : ℝ, 0 < y, y is again chosen after x, so y may depend on x. Does a suitable y need to depend on x?
Answer
No. y = 1 works for every x. The order of choices allows y to use x; the condition decides whether it has to. The Choices view cannot tell these two situations apart, because it leaves the condition out.
Exercise 1.5. Suppose the second statement were written ∃ b : ℝ, ∀ a : ℝ, a < b. Is it still false?
Answer
Yes. Renaming bound variables consistently does not change a statement. The Choices view would show the same two steps with the new labels. To change what is required you must change the structure: the order of the quantifiers or the condition.