<p><code>U : U</code> is inconsistent in a wide variety of settings. It is safe to say that it's inconsistent in any type theory. Deriving <code>False</code> from it is feasible by hand. The simplest version of this is called Hurkens' paradox:</p>
<ul>
<li><a href="https://github.com/agda/agda/blob/master/test/Succeed/Hurkens.agda" rel="nofollow noreferrer">Original source</a></li>
<li><a href="https://coq.inria.fr/stdlib/Coq.Logic.Hurkens.html" rel="nofollow noreferrer">Coq implementation</a>.</li>
<li><a href="https://github.com/agda/agda/blob/master/test/Succeed/Hurkens.agda" rel="nofollow noreferrer">Agda implementation</a>.</li>
</ul>
<p>The Coq source additionally describes the sufficient conditions for getting <code>False</code>. In short, we don't need <code>U : U</code>, it's enough to have two universes, where one is contained in the other, and both are closed under impredicative function types.</p>

CC BY-SA 4.0
2021-05-17T18:22:07.107Z
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?
Siddharth Bhat
CC BY-SA 4.0
2021-05-17T18:32:10.330Z
@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.
András Kovács
CC BY-SA 4.0
2021-05-17T18:39:16.123Z
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.
András Kovács
CC BY-SA 4.0
2021-05-18T08:46:15.233Z
@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.
PLL
CC BY-SA 4.0
2021-07-01T03:28:10.410Z
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.
Łukasz Lew
CC BY-SA 4.0
2021-05-17T18:17:43.840Z
2021-05-17T18:17:43.840Z
András Kovács
<p>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 <a href="https://en.wikipedia.org/wiki/Affine_logic" rel="nofollow noreferrer">Affine logic</a> Wikipedia entry.</p>
<blockquote>
<p>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.</p>
</blockquote>
<p>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, <a href="https://github.com/agda/agda/blob/989a13a3dc360f8355a1ea2ded9423b809b84ef6/test/Succeed/Hurkens.agda#L41" rel="nofollow noreferrer">this line</a> does not respect linearity.</p>

CC BY-SA 4.0
2021-05-17T22:11:43.740Z
2021-05-17T22:11:43.740Z
ice1000
<p>I am currently following <em><a href="http://davidchristiansen.dk/tutorials/nbe/" rel="nofollow noreferrer">Checking Dependent Types with Normalization by Evaluation: A Tutorial</a></em> by David Christiansen, where we consider the type of <code>U</code> (the universe of types) to be <code>U</code> itself [this can be seen section <code>7.4.1</code> in the implementation of <code>synth</code> where we have <code>['U (go '(the U U))]</code>: That is, the untyped expression <code>U</code> is elaborated into the expression <code>U</code> of type <code>U</code>. Effectively, we have taken that <code>Univ : Univ</code>.</p>
<p>This <a href="https://math.stackexchange.com/a/253823/261373">cannot happen in ZFC due to the axiom of foundation</a>. I suspect type-inferring <code>U</code> as having type <code>U</code> 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.</p>
<ul>
<li>Is it really true that <code>U : U</code> is inconsistent?</li>
<li>Is it possible to write a term that produces a proof of <code>False</code> assuming <code>U : U</code>? Or is the encoding to large to write down easily &quot;by hand&quot;, but can be believed to be done?</li>
<li>If <code>U : U</code> is <em>not</em> inconsistent (i.e., is consistent), then a couple of words on why the dependently typed world allows for <code>U : U</code> while ZFC cannot allow <code>U ∈ U</code> would be appreciated.</li>
</ul>
<p>I understand that talking about &quot;dependently typed languages&quot; is broad enough to be senseless. As a beginner, I find it hard to restrict to <em>one</em> 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.</p>

<type-theory><dependent-type>
Does univ : univ always lead to a contradiction in a dependently typed language?
Siddharth Bhat
# Does univ : univ always lead to a contradiction in a dependently typed language?

(Asked by: username_0 on 2021-05-17)

I am currently following *[Checking Dependent Types with Normalization by Evaluation: A Tutorial](http://davidchristiansen.dk/tutorials/nbe/)* 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](https://math.stackexchange.com/a/253823/261373). 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.

**Tags:** type-theory, dependent-type


---

## 2 answers

### Answer by username_1 on 2021-05-17. Score: 4 | Accepted answer

`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:

* [Original source](https://github.com/agda/agda/blob/master/test/Succeed/Hurkens.agda)
* [Coq implementation](https://coq.inria.fr/stdlib/Coq.Logic.Hurkens.html).
* [Agda implementation](https://github.com/agda/agda/blob/master/test/Succeed/Hurkens.agda).

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.

> **Comments:**
> **username_0**: 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?  
> **username_1**: @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.  
> **username_1**: 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.  
> **username_2**: @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.  
> **username_3**: 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.  

---

### Answer by username_4 on 2021-05-17. Score: 2

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](https://en.wikipedia.org/wiki/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](https://github.com/agda/agda/blob/989a13a3dc360f8355a1ea2ded9423b809b84ef6/test/Succeed/Hurkens.agda#L41) does not respect linearity.


---

