Zulip Chat Archive

Stream: general

Topic: A selfreferential paradox in Lean


Raphael Appenzeller (Jun 09 2022 at 07:19):

Consider the following definition: A real number xx is said to be conceivable if there is a Lean-program that defines xx and proves that xx 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 xx there is a .lean-file (x)\ell(x) and an associated integer i((x))i(\ell(x)) which is the number you get when you consider the .lean-file as a binary number in computer memory. The function ii \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 ii \circ \ell we can define a new conceivable number yy as follows: The nn th decimal digit of yy should always be 00 unless nn is in the image of ii \circ \ell and the conceivable number xx with i((x))i (\ell(x)) already has a 00 at its nn th decimal digit (in this case we set the nn th decimal digit of yy to be 11).
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 yy whose $$i(\ell(y))$$th digit has to be 00 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 (Jun 09 2022 at 07:21):

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 (Jun 09 2022 at 07:21):

Q1: no, you cannot define conceivable

Mario Carneiro (Jun 09 2022 at 07:21):

it would need to quantify over all universes

Eric Wieser (Jun 09 2022 at 07:22):

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

Mario Carneiro (Jun 09 2022 at 07:23):

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 (Jun 09 2022 at 07:24):

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 (Jun 09 2022 at 07:26):

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

Mario Carneiro (Jun 09 2022 at 07:26):

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

Mario Carneiro (Jun 09 2022 at 07:26):

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

Mario Carneiro (Jun 09 2022 at 07:27):

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

Eric Wieser (Jun 09 2022 at 07:27):

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 (Jun 09 2022 at 07:27):

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

Johan Commelin (Jun 09 2022 at 07:28):

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

Mario Carneiro (Jun 09 2022 at 07:28):

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 (Jun 09 2022 at 07:28):

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 (Jun 09 2022 at 07:29):

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

Mario Carneiro (Jun 09 2022 at 07:32):

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 (Jun 09 2022 at 07:33):

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

Mario Carneiro (Jun 09 2022 at 07:33):

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

Mario Carneiro (Jun 09 2022 at 07:34):

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 (Jun 09 2022 at 07:34):

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

Mario Carneiro (Jun 09 2022 at 07:35):

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 (Jun 09 2022 at 07:37):

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 (Jun 09 2022 at 07:46):

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 (Jun 09 2022 at 07:49):

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


Last updated: Dec 20 2023 at 11:08 UTC