2. Form a proposition, supply a proof

The two statements in Lesson 1 have different truth values, yet Lean accepts both as expressions. Your goal here is to explain what was accepted and then inspect evidence for the mathematical claims.

Read the declaration's type

These are complete Lean declarations:

example : Prop := ∀ x : Nat, ∃ y : Nat, y = x
example : Prop := ∃ y : Nat, ∀ x : Nat, y = x

In a declaration of the form example : T := value, the expression on the right must have type T. Here the required type is Prop, Lean's sort of propositions. Each right-hand side must therefore be a proposition.

Both succeed. A false proposition is still a proposition.

To supply a proof, put the proposition itself after the colon and provide a body with that type. The placement changes the task from forming a proposition to supplying its proof.

Construct the witness and its proof

theorem each_has_equal : ∀ x : Nat, ∃ y : Nat, y = x := by
  intro x
  exact ⟨x, rfl⟩

theorem names the result each_has_equal. After the colon is the proposition to prove. The by block constructs a proof.

Follow the two steps:

Step	What becomes available	What remains to establish
Before the proof steps	No particular natural number has been chosen.	For every `x`, there exists a suitable `y`.
`intro x`	An arbitrary `x : Nat`.	There exists `y : Nat` with `y = x`.
`exact ⟨x, rfl⟩`	The chosen witness is `x`; `rfl` proves reflexive equality.	The existential requirement is satisfied.

The notation ⟨x, rfl⟩ supplies both parts required by the existential claim: a witness and a proof of the condition for that witness. Merely naming a candidate would leave the condition unproved.

Exercise 2.1. If we used the candidate 0 for every input, what equality would still need a proof? Why does that candidate fail here?

Hint

Substitute 0 for y, leaving the arbitrary x unchanged.

Worked answer

We would need a proof of 0 = x for every natural number x. This fails, for example, at x = 1. The candidate is a natural number, but having the right type does not establish its required property.

Refute the other order

Lean can also check the argument that no single number equals every natural number:

theorem no_one_equals_all : ¬ (∃ y : Nat, ∀ x : Nat, y = x) := by
  intro h
  obtain ⟨y, hy⟩ := h
  have impossible : (0 : Nat) = 1 := (hy 0).symm.trans (hy 1)
  exact Nat.noConfusion impossible

The symbol ¬ means negation. To prove the negation, the proof assumes the existential statement as h and derives a contradiction.

obtain ⟨y, hy⟩ := h makes its proposed witness y and universal property hy available. Applying hy to 0 gives y = 0; applying it to 1 gives y = 1. Symmetry reverses the first equality, and transitivity combines them to obtain 0 = 1. The final line uses Lean's distinction between zero and a successor to rule out that equality.

You do not need to memorize these commands. The mathematical structure is the same as the worked answer in Lesson 1. Lean checks the supplied proof of that argument.

Test your reading of acceptance

Exercise 2.2. Classify each description:

Lean accepts example : Prop := ∃ y : Nat, ∀ x : Nat, y = x.
Lean accepts the body of each_has_equal at its declared proposition type.
The reader enters an existential body and introduces a candidate name.

Which establishes proposition formation? Which supplies a proof? Which is a step in reading a condition?

Worked answer

The first establishes that the expression forms a proposition. The second supplies a proof of the declared proposition in Lean's environment. The third introduces a candidate for reading the body; it does not establish an existential claim.

The distinctions remain necessary even if all three operations produce useful displays. Their outputs have different meanings.

Check the proof dependencies

Download QuantifierProofs.lean. It contains both proofs, followed by #print axioms commands. Under Lean 4.28.0, both named theorems report no axiom dependencies.

That is a claim about these particular proof terms. Later we will examine an accepted declaration whose proof contains a placeholder and whose dependency report is different.

For now, keep the declaration's required type in view. If it is Prop, the body forms a proposition. If it is a particular proposition, the body must supply a proof of that proposition.

← Follow the scope · Tutorial contents · Next: Follow an inspection →