2
$\begingroup$

I am currently following Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we consider the type of U (the universe of types) to be U itself [this can be seen section 7.4.1 in the implementation of synth where we have ['U (go '(the U U))]: That is, the untyped expression U is elaborated into the expression U of type U. Effectively, we have taken that Univ : Univ.

This cannot happen in ZFC due to the axiom of foundation. I suspect type-inferring U as having type U is inconsistent. I do not know how to prove this; I would attempt to encode a Russell-style paradox if I were pressed to produce a proof.

  • Is it really true that U : U is inconsistent?
  • Is it possible to write a term that produces a proof of False assuming U : U? Or is the encoding to large to write down easily "by hand", but can be believed to be done?
  • If U : U is not inconsistent (i.e., is consistent), then a couple of words on why the dependently typed world allows for U : U while ZFC cannot allow U ∈ U would be appreciated.

I understand that talking about "dependently typed languages" is broad enough to be senseless. As a beginner, I find it hard to restrict to one theory, because I don't know the trade-offs between the theories. For the sake of the answer, please feel free to restrict to, say, MLTT, or CoC, or LF.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
4
$\begingroup$

U : U is inconsistent in a wide variety of settings. It is safe to say that it's inconsistent in any type theory. Deriving False from it is feasible by hand. The simplest version of this is called Hurkens' paradox:

The Coq source additionally describes the sufficient conditions for getting False. In short, we don't need U : U, it's enough to have two universes, where one is contained in the other, and both are closed under impredicative function types.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you. To be painfully explicit: (1) the language implemented in the tutorial is not useful for proofs, since one can get a proof of False? (2) A way to remedy the situation is to introduce a universe hierarchy? $\endgroup$
    – Siddharth Bhat
    May 17, 2021 at 18:22
  • 2
    $\begingroup$ @SiddharthBhat I'd say it's useful for proofs. If you write a proof in an U : U theory, you have additional (informal) obligation to check that the proof is actually universe consistent, i.e. doesn't rely on size contradiction. In many cases, universe consistency is trivial to show, and everything else is more difficult. So an U : U proof assistant can be still quite helpful for getting evidence of validity. $\endgroup$
    – András Kovács
    May 17, 2021 at 18:32
  • 2
    $\begingroup$ Checked universe consistency of course bumps up the level of confidence one may have in a mechanized proof. I'd say there's a gradation: U : U proofs are far more trustworthy than informal proofs, and proofs in a consistent system are yet more so. In practice consistent systems are also actually inconsistent because of implementation bugs, so we don't get certainty, but that's not the point, the point is that we get proofs that are empirically far more reliable than informal proofs. $\endgroup$
    – András Kovács
    May 17, 2021 at 18:39
  • 2
    $\begingroup$ @AndrásKovács: regarding “ U:U proofs are more trustworthy than informal proofs” — I think this depends on who’s writing them. I know some people who are excellent mathematicians, but when formalising, lower their own care and rely on the proof-checker for correctness. From such people, I would trust their informal proofs more than their formal U:U proofs. $\endgroup$
    – PLL
    May 18, 2021 at 8:46
  • $\begingroup$ Is it true that all U:U proofs that strongly normalize are trustworthy or is there an incorrect proof that has a normal form? If it is the former, one could have a different mechanism than what we think of as types for ensuring termination. $\endgroup$
    – Łukasz Lew
    Jul 1, 2021 at 3:28
2
$\begingroup$

No, but only under a very specific condition (neither MLTT, or CoC, or LF) -- that your type theory has certain resource control mechanism (linear or affine). See Affine logic Wikipedia entry.

Affine logic predated linear logic. V. N. Grishin used this logic in 1974, after observing that Russell's paradox cannot be derived in a set theory without contraction, even with an unbounded comprehension axiom.

This is the only case I know that the construction of Girard's paradox would fail (theoretically). In AK's link to the Hurken's formalization, this line does not respect linearity.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.