When does DTT fail capturing things as intended?

Stream: Type theory

[Yiming Xu]

Hi, all. I am searching for examples of statements or proofs which makes sense in the usual mathematical language perfectly, but cannot be captured in DTT due to type-related reasons. For instance, one thing which only happens in DTT, but not usual mathematics, is the usage of universes. One of my naive guesses is that if a statement requires us to quantify over all universe levels, this will be problematic, and such an issue will not arise in mathematics on paper.

Or, is there any example that it is tricky to see that the formalisation in DTT agrees with its mathematical statement or the DTT version of it is "restricted" compared to the paper version?

I have one such example in HOL(to capture the precise math statement, it requires us to quantify over all types, impossible in simple type theory), but I do not have such an example for a system in DTT. As DTT is much more expressive than HOL, it is not surprising if such a case is very rare.

If you think some links are related to my question, thank you for sharing them as well!

[Kevin Buzzard]

Have you seen anyone quantifying over universes in paper mathematics? Universes are only used very rarely in standard paper mathematics; in fact for 2500 years we didn't use them at all and got on fine. When they are used nowadays they are typically used either to deal with category-theoretic issues (which could probably be overcome) or to reason about large cardinals (which you could do by just putting in an axiom that large cardinals exist in Type and then you wouldn't have to worry about universes; note that universes can't be proved to exist in ZFC so adding them as an axiom would not be considered odd by people who study them).

[Kevin Buzzard]

I have been pushing to do modern number theory in Lean and I've seen no examples of where a mathematical idea cannot be formalised in DTT in my research area; sometimes it takes a while to get it in in a way which is easy to use, but it always goes in in the end.

[Reid Barton]

This isn't exactly an example of "can't be formalized", but you might still be interested in this topic:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/CDGAs/near/167848869

[Kevin Buzzard]

One could argue that we know an awful lot more about that problem now than we did back then.

[Reid Barton]

Yes, I was going to ask about that, particularly with LTE doing homological algebra which hits some (but not all) of the same pain points

[Yiming Xu]

Kevin Buzzard said:

Have you seen anyone quantifying over universes in paper mathematics? Universes are only used very rarely in standard paper mathematics; in fact for 2500 years we didn't use them at all and got on fine. When they are used nowadays they are typically used either to deal with category-theoretic issues (which could probably be overcome) or to reason about large cardinals (which you could do by just putting in an axiom that large cardinals exist in Type and then you wouldn't have to worry about universes; note that universes can't be proved to exist in ZFC so adding them as an axiom would not be considered odd by people who study them).

I am not saying that I have examples of "paper mathematics" quantifying universes. Sorry for the confusion!
For such an example, a "model" (in the sense of logic, a model of a logic) on paper need an underlying set, but in HOL, as a set is of type "alpha -> bool", it is impossible to quantify on all the types, and hence all the sets, and hence impossible to quantify all the models. Therefore, even if we can prove that "for all models M, P(M)", it is impossible to be captured in HOL, instead, we can only say "for all alpha-model M (Models with underlying set type alpha), P(M)". Moreover, which matters is that: the requirement on the type-restriction here does become an issue during a proof, which can cause a statement failed to be proved.

[Yiming Xu]

And I am interested in the issues which can possibly be overcome due to category theory but remain a pain point now. If they are not such tricky to be stated, could you please give a bit examples on that? And I am also curious about the ones "takes quite a while" to get it in a way which is easy to use.

[Yiming Xu]

Reid Barton said:

This isn't exactly an example of "can't be formalized", but you might still be interested in this topic:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/CDGAs/near/167848869

Thanks for the link and I will try read it during the day!