A selfreferential paradox in Lean

Stream: general

[Raphael Appenzeller]

Consider the following definition: A real number $x$ is said to be conceivable if there is a Lean-program that defines $x$ and proves that $x$ is a real number.
Example: $\pi$ is conceivable, because the following Lean program exists:

import analysis.special_functions.exp
import data.set.intervals.infinite
import analysis.special_functions.trigonometric.basic
noncomputable theory
namespace real
   protected noncomputable def pi : ℝ := 2 * classical.some exists_cos_eq_zero
end real

Question 1: Is it possible to implement the definition of conceivable in Lean and to prove in Lean that $\pi$ is conceivable?
Now we argue that there can be at most countably many conceivable numbers: since for every conceivable number $x$ there is a .lean-file $\ell(x)$ and an associated integer $i(\ell(x))$ which is the number you get when you consider the .lean-file as a binary number in computer memory. The function $i \circ \ell$ is an injective function from the conceivable numbers to the natural numbers.
Question 2: Is it possible to implement in Lean the proof that there is an injective function from the conceivables to the naturals?
Now paradoxically we claim that the injection above cannot exist, by Cantor's diagonal argument: given the injection $i \circ \ell$ we can define a new conceivable number $y$ as follows: The $n$ th decimal digit of $y$ should always be $0$ unless $n$ is in the image of $i \circ \ell$ and the conceivable number $x$ with $i (\ell(x))$ already has a $0$ at its $n$ th decimal digit (in this case we set the $n$ th decimal digit of $y$ to be $1$).
Question 3: Is this new real number conceivable, i.e. is it possible to implement this definition (and the proof that it is a real number) in Lean?
If so, we have a conceivable number $y$ whose $$i(\ell(y))$$th digit has to be $0$ and nonzero at the same time, thus a contradiction.
Question 4: Is there a flaw in my intuitive argument for this contradiction?
Question 5: At which step is it no longer possible to implement the argument in Lean?

[Eric Wieser]

I'm pretty sure you can't prove anything about Lean in lean. What you can do is make a model of Lean in Lean, and prove things about that model

[Mario Carneiro]

Q1: no, you cannot define conceivable

[Mario Carneiro]

it would need to quantify over all universes

[Eric Wieser]

Can you elaborate on where universe quantification comes into play here?

[Mario Carneiro]

To say that a number is conceivable, you need to define a modeling relation between strings representing lean files and elements of the universe. This relation would have to involve arbitrarily large universes since you don't know in advance how many universes will be used in the construction of a given e.g. real number

[Mario Carneiro]

you could define something like "definable using only n universes" but there would be some definable numbers that are left out in this definition

[Eric Wieser]

Ah, so you're saying even with the "model of Lean in Lean" approach it's still not possible

[Mario Carneiro]

right, lean can't prove there exists a model of lean

[Mario Carneiro]

that's just a variation on Goedel's second incompleteness theorem

[Mario Carneiro]

lean can prove there exists a model of lean with only n universes though

[Eric Wieser]

What's the largest difference in mathlib between the universe of the type of a value and the universe needed to construct it?

[Mario Carneiro]

There is an old thread where I determined that the largest universe that appears in mathlib is 4

[Johan Commelin]

We still have a long way till we need 37 universes :rofl:

[Mario Carneiro]

but in the process I also found that there is an easy way to pump up the universe level of a definition by adding identity functions

[Eric Wieser]

Yes, that's what came to mind. My question was whether we have some things in Type 0 which rely on defs in Type 4 or similar

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Highest.20universe.20in.20mathlib/near/266024694

[Mario Carneiro]

The specific example there was that finsum_mem_empty.{0 0} is a definition (well, a theorem) which relies on definitions in Sort 4

[Kevin Buzzard]

I'm still skeptical of this claim. How do you see the 4?

[Mario Carneiro]

I go over it in detail in that thread (you were also skeptical then)

[Mario Carneiro]

It's not that I believe that this use is necessary, but rather that it is literally present if you unfold all the definitions

[Kevin Buzzard]

I think I failed to reproduce :-) I'll give it another go

[Mario Carneiro]

the challenge is to figure out how to formalize a lean model such that the really large universes are only "half-baked" in some as-yet-undetermined way such that they can validate games with id applications but such that they are not full models of ZFC

[Mario Carneiro]

I suspect that it suffices to say that the universes either don't support inductive types at all, or only "simple" inductive types (where "simple" is intended to exclude the really axiomatically strong examples like docs#pSet)

[Mario Carneiro]

By the way, in case you are wondering how there could be "more real numbers" if you tweak something as abstract as the number of universes used in the definition, consider this.

Real numbers are equivalent to sets of natural numbers so let's talk about those instead. An example of a nat -> Prop function which is not definable with fewer than n+1 universes is the truth predicate for formulas that talk about a model of lean with n universes. The existence of such a predicate implies the consistency of Lean_n, so Lean_n can't prove it exists and you need n+1 universes to prove it

[Mario Carneiro]

This phenomenon does not happen with nat, only real or nat -> Prop because nat is absolute but the powerset function is not.