<p>The 'logic' of the contradiction with <code>Type:Type</code> is that you can create a term of any type including 'empty' type by 'cheating' by never returning. This is essentially the only way to cheat because of subject reduction and the subformula properties. </p>

<p>Subject reduction states that evaluation of terms preserves their type.
If you have subject reduction and strong normalization (through whatever means), then you can infer that if you have a term of type <code>T</code>, you have a term of type <code>T</code> in a normal form - without any redexes (cuts) in it. </p>

<p>You have to go over all your type rules and verify that all of them have <a href="https://ncatlab.org/nlab/show/subformula+property" rel="noreferrer">subformula property</a> except the cut rule (which normalization eliminates). 
I.e you have to verify that if one of the non-cut rules were to produce a term of type <code>T</code> then you'll have one of its premises produce the term of type <code>T</code> (perhaps somewhere deeper in the derivation tree).
AFAIK every good type system requires sub-formula property (I'd like to learn of examples that contradict it).</p>

<p>Since type derivations are supposed to be finite trees, and you have no axiom (0 premises) rule to introduce a term of an empty type, you can prove by induction that no tree can build a term of an empty type. </p>

<p>To reiterate, the role of normalization is that cut rule does not have sub-formula property, so we have to eliminate it first while preserving the type of the term.</p>

<p>This is the general sketch of Gentzen's proofs of consistency of logics.</p>

CC BY-SA 4.0
2018-07-19T16:05:32.310Z
In order to do that, I would have to perform the work that I described that needs to be done on an unfamiliar set of rules linked by Maia. I'm not confident enough that I would not make a mistake.
Łukasz Lew
CC BY-SA 4.0
2018-07-19T16:06:18.403Z
Also, one might notice that I'm quite fuzzy about the subformula property, I would be happy to read some example of it in action.
Łukasz Lew
CC BY-SA 4.0
2018-07-19T16:06:23.443Z
Oh I see. Objection withdrawn then :)
Stella Biderman
CC BY-SA 4.0
2018-09-27T04:10:29.930Z
I love this answer, thanks for it! If I understand correctly, the cut rule for linear λ-calculus is better in that sense since it has the subformula property, right?
MaiaVictor
CC BY-SA 4.0
2018-09-27T22:04:08.103Z
Cut rule (even linear) does not have sub-formula property since the cut-out formula is disappearing. That's why cut elimination (even in linear logic) is so important.
Łukasz Lew
CC BY-SA 4.0
2018-07-19T00:54:00.687Z
2018-07-19T00:54:00.687Z
Łukasz Lew
<h3>Question</h3>

<p>If a pure type system has a terminating proof language, can we have <code>Type : Type</code> at the logic level without causing paradoxes (i.e., without causing <code>∀ (x : *) -&gt; x</code> to be inhabited)?</p>

<h3>Example</h3>

<p>Suppose we take a pure type theory such as the Calculus of Constructions, restrict functions to be affine (at most 1 variable uses) and add constructs for stratified duplications - see <a href="https://gist.github.com/MaiaVictor/b555a0913317622a8bf8f06b526b0722" rel="noreferrer">here</a> for details. That language - which we could call EACC (Elementary Affine Calculus of Constructions) has a normalizing untyped fragment. That is, the reduction of any term - even ill-typed ones - is guaranteed to terminate due to the reduction rules (and, in particular, the restriction that duplicated terms can not change their levels).</p>

CC BY-SA 4.0
2018-07-18T16:31:27.280Z
Perhaps "Is `Type : Type` possible in an affine type theory?" is a better title?
Andrej Bauer
CC BY-SA 4.0
2018-07-18T17:29:57.147Z
@AndrejBauer perhaps it needs a better body actually, I used EAL as an example but the actual question is if a terminating proof language makes `Type : Type` possible.
MaiaVictor
CC BY-SA 4.0
2018-07-19T14:20:50.630Z
For basic type:type background I found these helpful:
http://www.konne.me/2015/08/17/paradoxes.html
The coq source is in his github repo https://github.com/konne88/konne88.github.io . 
There is also a very nice agda version: https://gist.github.com/favonia/cc7a504839c5fbb3ebc6
user833970
CC BY-SA 4.0
2018-07-19T18:48:46.177Z
I'd like to try to look with more detail into your EACC. Are variables classified into affine and non-affine? Do these form separate environments? Why strange syntax with '$'. "$v x y" = "let v = x in y" right? Is v required to be affine?
Łukasz Lew
CC BY-SA 4.0
2018-08-12T00:36:12.207Z
I think that in Coquand's "An Analysis of Girard's Paradox" he shows a type system (from Martin Lof) with type:type which is terminating but where every type has an inhabitant.
user833970
<type-theory><lambda-calculus><dependent-type>
If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?
MaiaVictor
# If the untyped language is terminating, can we still derive a contradiction from `Type : Type`?

(Asked by: username_0 on 2018-07-18)

### Question

If a pure type system has a terminating proof language, can we have `Type : Type` at the logic level without causing paradoxes (i.e., without causing `∀ (x : *) -> x` to be inhabited)?

### Example

Suppose we take a pure type theory such as the Calculus of Constructions, restrict functions to be affine (at most 1 variable uses) and add constructs for stratified duplications - see [here](https://gist.github.com/MaiaVictor/b555a0913317622a8bf8f06b526b0722) for details. That language - which we could call EACC (Elementary Affine Calculus of Constructions) has a normalizing untyped fragment. That is, the reduction of any term - even ill-typed ones - is guaranteed to terminate due to the reduction rules (and, in particular, the restriction that duplicated terms can not change their levels).

**Tags:** type-theory, lambda-calculus, dependent-type
> **Comments:**
> **username_1**: Perhaps "Is `Type : Type` possible in an affine type theory?" is a better title?  
> **username_0**: @AndrejBauer perhaps it needs a better body actually, I used EAL as an example but the actual question is if a terminating proof language makes `Type : Type` possible.  
> **username_2**: For basic type:type background I found these helpful: http://www.konne.me/2015/08/17/paradoxes.html The coq source is in his github repo https://github.com/konne88/konne88.github.io .  There is also a very nice agda version: https://gist.github.com/favonia/cc7a504839c5fbb3ebc6  
> **username_3**: I'd like to try to look with more detail into your EACC. Are variables classified into affine and non-affine? Do these form separate environments? Why strange syntax with '$'. "$v x y" = "let v = x in y" right? Is v required to be affine?  
> **username_2**: I think that in Coquand's "An Analysis of Girard's Paradox" he shows a type system (from Martin Lof) with type:type which is terminating but where every type has an inhabitant.  

---

## 1 answers

### Answer by username_3 on 2018-07-19. Score: 8 | Accepted answer

The 'logic' of the contradiction with `Type:Type` is that you can create a term of any type including 'empty' type by 'cheating' by never returning. This is essentially the only way to cheat because of subject reduction and the subformula properties.

Subject reduction states that evaluation of terms preserves their type.
If you have subject reduction and strong normalization (through whatever means), then you can infer that if you have a term of type `T`, you have a term of type `T` in a normal form - without any redexes (cuts) in it.

You have to go over all your type rules and verify that all of them have [subformula property](https://ncatlab.org/nlab/show/subformula+property) except the cut rule (which normalization eliminates).
I.e you have to verify that if one of the non-cut rules were to produce a term of type `T` then you'll have one of its premises produce the term of type `T` (perhaps somewhere deeper in the derivation tree).
AFAIK every good type system requires sub-formula property (I'd like to learn of examples that contradict it).

Since type derivations are supposed to be finite trees, and you have no axiom (0 premises) rule to introduce a term of an empty type, you can prove by induction that no tree can build a term of an empty type.

To reiterate, the role of normalization is that cut rule does not have sub-formula property, so we have to eliminate it first while preserving the type of the term.

This is the general sketch of Gentzen's proofs of consistency of logics.

> **Comments:**
> **username_3**: In order to do that, I would have to perform the work that I described that needs to be done on an unfamiliar set of rules linked by Maia. I'm not confident enough that I would not make a mistake.  
> **username_3**: Also, one might notice that I'm quite fuzzy about the subformula property, I would be happy to read some example of it in action.  
> **username_4**: Oh I see. Objection withdrawn then :)  
> **username_0**: I love this answer, thanks for it! If I understand correctly, the cut rule for linear λ-calculus is better in that sense since it has the subformula property, right?  
> **username_3**: Cut rule (even linear) does not have sub-formula property since the cut-out formula is disappearing. That's why cut elimination (even in linear logic) is so important.  

---

