unique typing

Stream: general

[Mario Carneiro]

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]

Any chance it's a Lean proof?

[Moses Schönfinkel]

Good one.

[Mario Carneiro]

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]

Wouldn't a Lean formalization be self-referential?

[Mario Carneiro]

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]

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]

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]

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

No.

[Kevin Buzzard]

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

[Gabriel Ebner]

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]

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.intros, 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]

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]

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]

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]

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]

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

[Andrew Ashworth]

not totally related but possibly humorous

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

Hmm let me dig out the quote.

[Kevin Buzzard]

section 3.7

[Kevin Buzzard]

"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]

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]

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

[Kevin Buzzard]

Oh I see!

[Kevin Buzzard]

Is that your thesis problem?

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Like I said, big guns

[Mario Carneiro]

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

[Kevin Buzzard]

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]

If mathematics = lean, sure :)

[Kevin Buzzard]

beyond mathematics, rather than advanced mathematics

[Kevin Buzzard]

Oh, mathematics is ZFC :-)

[Kevin Buzzard]

Of this there is little doubt

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

And there's also some section in the stacks project

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Those are just the amateurs

[Mario Carneiro]

like Wiles, I think

[Kevin Buzzard]

Yup

[Kevin Buzzard]

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

[Kevin Buzzard]

This is how mathematics is actually done in 2018.

[Kevin Buzzard]

It's farcical.

[Kevin Buzzard]

We all believe we're working in ZFC

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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