# Zulip Chat Archive

## Stream: general

### Topic: unique typing

#### Mario Carneiro (Mar 15 2018 at 11:27):

Success! I managed to finally show that Lean's full type system has unique typing (which implies stuff like it is impossible to prove `Type 0 : Type 0`

), even if you use "full" definitional equality, i.e. the transitive and undecidable ideal version of what lean checks. Since it uses a reduction that is guaranteed to run forever on subsingleton eliminators like `acc`

, it yields an alternative semi-decision procedure for testing definitional equality.

#### Simon Hudon (Mar 15 2018 at 12:18):

Any chance it's a Lean proof?

#### Moses Schönfinkel (Mar 15 2018 at 12:19):

Good one.

#### Mario Carneiro (Mar 15 2018 at 12:22):

No, it's still in the informal stage, although the proof is sufficiently subtle that it might be a good idea to formalize it just to make sure it all actually works as advertised.

#### Patrick Massot (Mar 15 2018 at 12:24):

Wouldn't a Lean formalization be self-referential?

#### Mario Carneiro (Mar 15 2018 at 12:30):

Sure, but it wouldn't be the first time a proof assistant has proven parts of itself. Also unique typing is weaker than soundness - even if the type system is inconsistent there are many things that can't be defeq. I did not need to assume any inaccessible cardinals in the proof, it's a purely syntactic proof

#### Simon Hudon (Mar 15 2018 at 12:39):

I guess even if self-referential, it might be a good way to find errors. You might want to write it in Isabelle (or something else) if you want to avoid the self-referential criticism but even Lean would help get the details right

#### Kevin Buzzard (Mar 15 2018 at 14:40):

Does your work shed any light on whether it is possible to make Lean's definitional equality "better" whilst still remaining decidable? Actually here is an even dumber question. Is the transitive closure of Lean's definitional equality still decidable? One's first thought is "of course not, if you want to prove `x=y`

by finding `z`

such that `x=z`

and `z=y`

then where do you start?", but if transitivity somehow only fails in some controlled way then perhaps there is some algorithm which spits out sensible choices for `z`

.

#### Gabriel Ebner (Mar 15 2018 at 14:42):

Is the transitive closure of Lean's definitional equality still decidable?

No.

#### Kevin Buzzard (Mar 15 2018 at 14:43):

This doesn't surprise me at all. How does one go about proving this?

#### Gabriel Ebner (Mar 15 2018 at 14:43):

It's the standard interaction between subsingleton elimination (in particular `acc.rec`

) and proof irrelevancy. See also https://leanprover.github.io/reference/expressions.html#computation

#### Gabriel Ebner (Mar 15 2018 at 14:47):

The trick is that 1) you can encode functions with unbounded recursion using well-founded recursion (where the proof is e.g. exfalso), 2) you can evaluate such functions as many steps as you have nested `acc.intro`

s, 3) by proof irrelevancy all such `acc.intro`

terms are definitionally equal. You can for example now ask whether the original function returns `0`

when given `0`

using a definitional equality test, and this problem is undecidable.

#### Kevin Buzzard (Mar 15 2018 at 14:50):

Thanks for the added information. This will greatly decrease the amount of time it will take to me to understand your previous comment :-) I'm sure this is standard DTT stuff but I am still a beginner. Thanks.

#### Kevin Buzzard (Mar 15 2018 at 14:52):

Aah so in fact this seems to be exactly the trick used to show that defeq isn't transitive in the reference manual. I have never taken the time to understand that proof before -- I just verified that it worked and moved on. I think that at the time I knew so little Lean that it just looked too daunting to get to the bottom of.

#### Mario Carneiro (Mar 15 2018 at 21:13):

Does your work shed any light on whether it is possible to make Lean's definitional equality "better" whilst still remaining decidable?

The proof does a good job of pointing the finger squarely at subsingleton eliminators. That is, if there were no inductive types such that:

- The inductive type is a Prop family
- The inductive type has one constructor
- The constructor has at least one non-prop argument
- The constructor has at least one recursive argument
- All non-prop arguments appear in the output type

then definitional equality would be decidable.

#### Mario Carneiro (Mar 15 2018 at 21:15):

Probably the same can be said about proof irrelevance, but that's baked in a bit more thoroughly, so it's less obvious how it would change the proof.

#### Andrew Ashworth (Mar 15 2018 at 21:41):

i was searching "subsingleton elimination" and one of the top results was this: https://www.cs.cmu.edu/~cangiuli/sigbovik/unintentional.pdf

#### Andrew Ashworth (Mar 15 2018 at 21:41):

not totally related but possibly humorous

#### Mario Carneiro (Mar 15 2018 at 21:42):

Oh, I was wrong about needing at least one non-prop argument. Here's an extremely simple type, simpler than `acc`

, that also causes the same problems (non-transitivity, undecidability)

inductive T : Prop | mk : T → T variables (x : T) {α : Sort*} (f : α → α) def fix : α := T.rec (λ _, f) x example : fix x f = f (fix x f) := show fix (T.mk x) f = f (fix x f), from rfl

#### Kevin Buzzard (Mar 15 2018 at 22:35):

You have a variable of type `T`

but I am not sure it's possible to construct anything of type T.

variable y : false example : false := y

This has caused a lot more trouble than undecidability. I don't really understand what you're saying yet but I am still optimistic it's within my grasp. You seem to have proved that every function has a fixed point, given a variable of type `T`

, a type for which there are no instances. What does this have to do with non-transitivity and undecidability? Sorry if this is all standard.

#### Mario Carneiro (Mar 15 2018 at 22:50):

That's correct - I didn't mention it but `(x : T)`

is an inconsistent context. `fix`

is also inconsistent, but from a soundness perspective that's no surprise, inconsistent in, inconsistent out. The point is that this is a fixpoint operation that works definitionally, so I can execute unbounded computations exactly as one might use `fix`

in haskell. For example, let `f : (nat -> unit) -> (nat -> unit)`

such that `f g n := if TM halts at n then () else g (n+1)`

, then `fix f 0`

evaluates all the steps of a turing machine, resulting in `()`

if and only if the TM halts, so `fix x f 0 =?= ()`

is undecidable.

#### Mario Carneiro (Mar 15 2018 at 22:53):

Note that the other known examples of undecidable definitional equality problems also occur in inconsistent contexts. I'm not certain if it suffices to assume the context is consistent, but if "consistent" is replaced by "inhabited" (i.e. there is a concrete sequence of terms which satisfies the context) then it is equivalent to asking if reduction terminates in the empty context, which is also known as strong normalization. This is believed to be true, but I guess that will be another big chapter

#### Kevin Buzzard (Mar 15 2018 at 22:59):

Strong Normalization is an open problem -- is that correct? I read it in the reference manual I guess. It feels to me a bit like the 3n+1 problem :-)

#### Mario Carneiro (Mar 15 2018 at 23:00):

I don't think it is, although you have to pull out the big guns to prove it, since it implies that lean is consistent

#### Kevin Buzzard (Mar 15 2018 at 23:00):

Hmm let me dig out the quote.

#### Kevin Buzzard (Mar 15 2018 at 23:01):

section 3.7

#### Kevin Buzzard (Mar 15 2018 at 23:01):

"The reduction relation is believed to be strongly normalizing, which is to say, every sequence of reductions applied to a term will eventually terminate."

#### Mario Carneiro (Mar 15 2018 at 23:01):

These definitional equality problems are a little counter intuitive, because you want to reason that in an inconsistent context anything goes, but that's actually not the case. Even if you prove `0 = 1`

, you still cannot prove that `0 == 1`

definitionally

#### Mario Carneiro (Mar 15 2018 at 23:02):

"Believed to be" is code for "no one's done the work". That's my job :)

#### Kevin Buzzard (Mar 15 2018 at 23:02):

Oh I see!

#### Kevin Buzzard (Mar 15 2018 at 23:02):

Is that your thesis problem?

#### Mario Carneiro (Mar 15 2018 at 23:03):

It's one of the nearby problems, I'm not quite sure what my thesis will be exactly but something along these lines

#### Mario Carneiro (Mar 15 2018 at 23:03):

I guess it depends on what I get done, but unique typing is a major step forward

#### Mario Carneiro (Mar 15 2018 at 23:04):

soundness is the next step, by modeling everything in ZFC + omega inaccessibles

#### Mario Carneiro (Mar 15 2018 at 23:05):

then strong normalization, where you use the rank of a term's ZFC interpretation as the wellfounded decreasing measure

#### Kevin Buzzard (Mar 15 2018 at 23:05):

I think that modeling Lean in ZFC + omega inaccessibles is how I initially tried to understand type theoy.

#### Kevin Buzzard (Mar 15 2018 at 23:06):

Assuming that inductive structures don't add a bunch of axioms I wasn't expecting, this sounds straightforward to me and is probably all well-known. Is that right?

#### Mario Carneiro (Mar 15 2018 at 23:06):

That's actually the easiest part, it's quite straightforward. But there are some places where I need to know that if a term is a Prop then it's not a Type, and unique typing was necessary for that

#### Kevin Buzzard (Mar 15 2018 at 23:07):

Oh so you use all this to prove strong normalization??

#### Kevin Buzzard (Mar 15 2018 at 23:07):

I thought you were just going to argue by induction on number of unicode characters in the term :-)

#### Mario Carneiro (Mar 15 2018 at 23:07):

Like I said, big guns

#### Mario Carneiro (Mar 15 2018 at 23:08):

remember from Godel that anything that implies Con(lean) is going to require some advanced mathematics

#### Kevin Buzzard (Mar 15 2018 at 23:08):

I know people who would say that anything that implies Con(lean) is going to require something that is strictly stronger than mathematics

#### Mario Carneiro (Mar 15 2018 at 23:09):

If mathematics = lean, sure :)

#### Kevin Buzzard (Mar 15 2018 at 23:09):

beyond mathematics, rather than advanced mathematics

#### Kevin Buzzard (Mar 15 2018 at 23:09):

Oh, mathematics is ZFC :-)

#### Kevin Buzzard (Mar 15 2018 at 23:09):

Of this there is little doubt

#### Mario Carneiro (Mar 15 2018 at 23:09):

You don't believe in the existence of grothendieck universes?

#### Kevin Buzzard (Mar 15 2018 at 23:10):

in the sense that 90% of mathematicians don't have a clue what mathematics is but know how to use it, 9.9% know what ZFC is and use that, and then the other 0.1% worry about other possibilities.

#### Kevin Buzzard (Mar 15 2018 at 23:10):

Didn't I share that link from a recent Scholze paper recently?

#### Kevin Buzzard (Mar 15 2018 at 23:10):

And there's also some section in the stacks project

#### Kevin Buzzard (Mar 15 2018 at 23:10):

Real, serious, mathematicians actually occasionally go out of their way to justify to the rest of the world that what they are doing can be done in ZFC

#### Mario Carneiro (Mar 15 2018 at 23:11):

I always get the sense from regular mathematicians that if large cardinals come up they just assume them and move on

#### Kevin Buzzard (Mar 15 2018 at 23:11):

Those are just the amateurs

#### Mario Carneiro (Mar 15 2018 at 23:11):

like Wiles, I think

#### Kevin Buzzard (Mar 15 2018 at 23:11):

Yup

#### Kevin Buzzard (Mar 15 2018 at 23:11):

He doesn't know how to remove it, but he knows who to ask

#### Kevin Buzzard (Mar 15 2018 at 23:12):

This is how mathematics is actually done in 2018.

#### Kevin Buzzard (Mar 15 2018 at 23:12):

It's farcical.

#### Kevin Buzzard (Mar 15 2018 at 23:12):

We all believe we're working in ZFC

#### Kevin Buzzard (Mar 15 2018 at 23:13):

and occasionally someone writes a chapter in a paper saying "I know section 5 was full of categories of rings, but actually we could look at the category of rings which live in V_kappa for kappa=2^2^2^2^2^2^aleph_0 and it all still works, so it's OK we're doing ZFC"

#### Kevin Buzzard (Mar 15 2018 at 23:13):

and then all of us amateurs go "oh that's a relief, it's still holding out"

#### Kevin Buzzard (Mar 15 2018 at 23:15):

http://www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf

#### Kevin Buzzard (Mar 15 2018 at 23:15):

one of the best living mathematicians, 2017 paper, check out section 4

#### Kevin Buzzard (Mar 15 2018 at 23:17):

Algebraic geometry genius Johan de Jong's stacks project: https://stacks.math.columbia.edu/tag/000F and https://stacks.math.columbia.edu/tag/000H

#### Kevin Buzzard (Mar 15 2018 at 23:17):

All of that crap just so we can say "it's OK, we're still in ZFC"

#### Kevin Buzzard (Mar 15 2018 at 23:20):

What's happening is that large cardinals come up (99% of the time in the form "this functor from the category of rings to the category of sets is representable") and people either say nothing (the normal situation) or they note that functors are a bit problematic in ZFC but they read somewhere in the stacks project that it was all OK, or maybe Brian Conrad told them once. There is no formal reference that "everything is OK", but people know who to ask if they're worried

#### Kevin Buzzard (Mar 15 2018 at 23:21):

Over the last year I have come to regard this position as farcical. What are the point of foundations? They're to make your life easier! Not so Scholze has to take time out from being a father of 2 small kids and generating a pile of amazing arithmetic algebraic geometry so he can write down some crap about cardinals just to prove that his latest theory fits into ZFC.

#### Mario Carneiro (Mar 15 2018 at 23:23):

As far as Con(lean) is concerned, the easy/lazy approach (that I will take, at least at first) is to assume omega inaccessibles and prove it. You can be more refined though, since for a specific proof you only need n inaccessibles for some n < omega. It might be possible to even trim down the universes themselves so that they aren't quite grothendieck universes, and then maybe you can fit it all in ZFC, but this probably fails in some extreme cases (like when constructing a model of ZFC in lean)

#### Mario Carneiro (Mar 15 2018 at 23:46):

By the way, https://www.fing.edu.uy/~amiquel/publis/types02.pdf "The not so simple proof-irrelevant model of CC" is my competition in the soundness part; I contend that it is exactly as simple as it looks, and they made some poor modeling decisions in there that made things complicated

Last updated: May 11 2021 at 22:14 UTC