<p>It is actually possible to relax strict positivity and remain consistent. For instance, it suffices to only have a positivity condition. That is, we can accept type definitions like</p>

<p>$$
  T \triangleq \mu\alpha. (\alpha \to 2) \to 2
$$</p>

<p>where recursive type variables occur to the left of an even number of arrows and retain consistency.</p>

<p>However, theories permitting this sort of inductive type do not have set-theoretic models -- you cannot interpret types as sets and terms as elements of sets. In this case, we are saying that $T$ is isomorphic to its double-powerset (i.e., $T \simeq \mathcal{P}(\mathcal{P}(T))$), and this violates <a href="http://en.wikipedia.org/wiki/Cantor%27s_theorem">Cantor's theorem</a>. </p>

<p>Since dependent type theories are often used to formalize mathematics, their designers are usually hesitant to add principles which are not compatible with a set-theoretic semantics, even if they are consistent.</p>

<p>EDIT: I'm adding this edit in response to Andrej's question. The type $T$ <em>is consistent</em> if you add it to (say) Agda; there are no problems with it at all. We only have a problem if we combine non-strict positivity with excluded middle.</p>

<p>The intuition for why is safe is (IMO) best seen through the lens of parametricity. In System F, we can show using parametricity that for any definable functor $F$, the type $\mu F \triangleq \forall \alpha.\; (F\alpha \to \alpha) \to \alpha$ is indeed an inductive type. </p>

<p>Now, recall that a definable functor $F$ is a type operator $F : \ast \to \ast$, together with an operator 
$$\mathrm{map} : \forall \alpha,\beta.\;(\alpha \to \beta) \to F\;\alpha \to F\;\beta$$
satisfying the functoriality conditions (i.e., $\mathrm{map}\;id = id$ and $\mathrm{map}\;f\;\circ \mathrm{map}\;g = \mathrm{map}\;(f \circ g$). </p>

<p>Now, we can define a type operator for the double powerset</p>

<p>$$C = \lambda \alpha.\; (\alpha \to 2) \to 2$$</p>

<p>and because $\alpha$ occurs only positively, we can also define a map operator for it:</p>

<p>$$
map_C = \lambda f : \alpha \to \beta, a' : (\alpha \to 2) \to 2, k : \beta \to 2.\; a' \;(\lambda a:\alpha.\; k\;(f\;a))
$$</p>

<p>So we know that $T = \mu C$ is a legitimate inductive type. </p>

CC BY-SA 3.0
2014-04-02T09:24:35.110Z
Can we come up with an example which creates an inconsistency all by itself? Your example is inconsistent if we also assume (enough) excluded middle.
Andrej Bauer
CC BY-SA 3.0
2014-04-02T10:22:46.213Z
Another reason is that we can add the FAN theorem to Agda, after which we can prove that the type in question is (isomorphic to) natural numbers.
Andrej Bauer
CC BY-SA 3.0
2014-04-02T10:23:25.013Z
I am thinking $\mu \alpha . (\alpha \to 2) \to \alpha$ should be pretty bad.
Andrej Bauer
CC BY-SA 3.0
2014-04-02T11:07:15.747Z
Ah, I misunderstood the question -- the point is that strict positivity is a sufficient but not necessary condition. Your example (with an actual negative occurence) is inconsistent.
Neel Krishnaswami
CC BY-SA 3.0
2014-04-02T12:08:20.070Z
Yeah, I just realized that. My example doesn't hold water.
Andrej Bauer
CC BY-SA 3.0
2014-04-02T09:09:19.030Z
2014-04-02T09:42:17.933Z
2014-04-02T09:42:17.933Z
Neel Krishnaswami
<p>Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?</p>

<lo.logic><type-theory><dependent-type>
Example of where violation of strict positivity condition in inductive types leads to inconsistency
Konstantin Solomatov
# Example of where violation of strict positivity condition in inductive types leads to inconsistency

(Asked by: username_0 on 2014-04-01)

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?

**Tags:** lo.logic, type-theory, dependent-type

---

## 1 answers

### Answer by username_1 on 2014-04-02. Score: 11 | Accepted answer

It is actually possible to relax strict positivity and remain consistent. For instance, it suffices to only have a positivity condition. That is, we can accept type definitions like

$$
T \triangleq \mu\alpha. (\alpha \to 2) \to 2
$$

where recursive type variables occur to the left of an even number of arrows and retain consistency.

However, theories permitting this sort of inductive type do not have set-theoretic models -- you cannot interpret types as sets and terms as elements of sets. In this case, we are saying that $T$ is isomorphic to its double-powerset (i.e., $T \simeq \mathcal{P}(\mathcal{P}(T))$), and this violates [Cantor's theorem](http://en.wikipedia.org/wiki/Cantor%27s_theorem).

Since dependent type theories are often used to formalize mathematics, their designers are usually hesitant to add principles which are not compatible with a set-theoretic semantics, even if they are consistent.

EDIT: I'm adding this edit in response to Andrej's question. The type $T$ *is consistent* if you add it to (say) Agda; there are no problems with it at all. We only have a problem if we combine non-strict positivity with excluded middle.

The intuition for why is safe is (IMO) best seen through the lens of parametricity. In System F, we can show using parametricity that for any definable functor $F$, the type $\mu F \triangleq \forall \alpha.\; (F\alpha \to \alpha) \to \alpha$ is indeed an inductive type.

Now, recall that a definable functor $F$ is a type operator $F : \ast \to \ast$, together with an operator
$$\mathrm{map} : \forall \alpha,\beta.\;(\alpha \to \beta) \to F\;\alpha \to F\;\beta$$
satisfying the functoriality conditions (i.e., $\mathrm{map}\;id = id$ and $\mathrm{map}\;f\;\circ \mathrm{map}\;g = \mathrm{map}\;(f \circ g$).

Now, we can define a type operator for the double powerset

$$C = \lambda \alpha.\; (\alpha \to 2) \to 2$$

and because $\alpha$ occurs only positively, we can also define a map operator for it:

$$
map\_C = \lambda f : \alpha \to \beta, a' : (\alpha \to 2) \to 2, k : \beta \to 2.\; a' \;(\lambda a:\alpha.\; k\;(f\;a))
$$

So we know that $T = \mu C$ is a legitimate inductive type.

> **Comments:**
> **username_2**: Can we come up with an example which creates an inconsistency all by itself? Your example is inconsistent if we also assume (enough) excluded middle.  
> **username_2**: Another reason is that we can add the FAN theorem to Agda, after which we can prove that the type in question is (isomorphic to) natural numbers.  
> **username_2**: I am thinking $\mu \alpha . (\alpha \to 2) \to \alpha$ should be pretty bad.  
> **username_1**: Ah, I misunderstood the question -- the point is that strict positivity is a sufficient but not necessary condition. Your example (with an actual negative occurence) is inconsistent.  
> **username_2**: Yeah, I just realized that. My example doesn't hold water.  

---

