1. Follow the scope
Your goal is to explain why swapping two quantifiers changes what a statement requires. We will use natural numbers, including zero, and ordinary equality.
A separate choice for each input
Read this expression from left to right:
#check ∀ x : Nat, ∃ y : Nat, y = x
#check asks Lean to report an expression's type; it does not ask Lean to prove the expression. Nat is Lean's type of natural numbers. The symbol ∀ means “for every,” and ∃ means “there exists.” The statement says:
For every natural number
x, there is a natural numberyequal tox.
The names following quantifiers are bound variables. A binder introduces a name and the part of the expression in which that name is available: its scope.
Here x is introduced first. Inside its scope, the statement requires a suitable y. This allows the choice of y to depend on x.
For x = 2, choose y = 2. For x = 7, choose y = 7. You do not have to keep the same choice of y for different values of x.
Exercise 1.1. Choose y when x = 0 and when x = 12. Then give a rule that works for an arbitrary x.
Hint
The condition asks for equality. Use the input itself.
Worked answer
Choose 0 and 12, respectively. In general, choose y to be x. The equality then reads x = x, which holds by reflexivity.
Checking two inputs only illustrates the rule. The argument covers every input because it describes a valid choice and establishes the required equality for an arbitrary x.
One choice for every input
Now swap the quantifiers:
#check ∃ y : Nat, ∀ x : Nat, y = x
This says:
There is a natural number
ysuch that, for every natural numberx,y = x.
The existential choice is now outside the universal quantifier. One y must satisfy all its requirements. You may choose y knowing that the universal requirement is coming, but you cannot choose a different y for each x.
This is an explanatory diagram of scope, not a captured Definograph view. Nesting represents which names are available; it does not certify either statement.
Exercise 1.2. Suppose such a y exists. What happens when you apply its requirement to x = 0 and then to x = 1?
Hint
Keep the same y in both equalities.
Worked answer
The requirement gives y = 0 and y = 1. These imply 0 = 1, a contradiction. Therefore no such y exists.
This is stronger than trying some choices and failing to find a witness. Any proposed witness would have to satisfy both incompatible requirements.
Read the difference precisely
| Statement | Allowed dependence | Requirement |
|---|---|---|
∀ x : Nat, ∃ y : Nat, y = x | The choice of y may depend on x. | Find an equal number for each input. |
∃ y : Nat, ∀ x : Nat, y = x | One y must work throughout the universal statement. | Find a number equal to every natural number. |
Saying “may depend” matters. An existential quantifier inside a universal quantifier permits dependence; it does not demand different witnesses whenever the input changes. For example, the requirement y = 0 would allow the constant choice 0 for every x.
Separate a name from its role
Compare the first statement with:
#check ∀ input : Nat, ∃ output : Nat, output = input
The names are longer, but the dependency and requirement are the same. What matters is which binder each occurrence refers to and where that binder has scope.
Exercise 1.3. Does renaming x to input and y to output repair the false, second statement?
Worked answer
No. Consistently changing bound-variable names preserves the statement's meaning. To change the requirement here, you must change the structure, such as the order of the quantifiers or the equality they govern.
Definograph's reading must preserve these same relationships. Introducing an existential candidate while inspecting its condition helps us read that condition. It does not find a witness or prove that one exists.
Check the expressions
The download Scope.lean contains these expressions and the constant-choice example. With Lean 4.28.0, each #check reports a type of Prop, including the false statement. That observation is the starting point of the next lesson.