8
$\begingroup$

System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox.

One-sorted circular PTS $\lambda\ast$ ($S = \{\ast \}, A=\{\ast\colon \ast\}, R=\{(\ast,\ast)\}$) (Geuvers' Logics and Type Systems, p.78) is also inconsistent since a term of type $\bot$ in System U can be translated into $\lambda\ast$ by mapping $\ast, \square$ and $\triangle$ to $\ast$.

Is there any easier way to construct a term of type $\bot$ in $\lambda\ast$? Smaller terms, or constructions easier to understand, are appreciated.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
9
$\begingroup$

I feel like most of my posts on mathoverflow and cstheory.stackexchange consist of this answer, but the most perspicuous (in my opinion) proof of inconsistency of U and $*:*$ is a construction by Alexandre Miquel, given in his phd dissertation. Tragically, it is in French, so I'll summarize the idea below, and maybe you'll be able to fill in the remainder using his other paper lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts..

The idea is to build a model of naive set theory in $*:*$. The naive theory allows for unrestricted comprehension, and in particular the paradox falls out quite easily. The proof term of $\bot$ itself is longer than in Hurkens' presentation, but I think it's safe to say that the process is at least more straightforward.

The crucial idea is to model a set as a directed pointed graph. The point represents the set, the graph contains all the members of the set, and the membership relation is represented by the edges. We rely on the encoding of $\Sigma$ types in the impredicative theories.

A set $S$ is thus an element of

$$\mathrm{Set}=\Sigma (A:*)(x :A)(R:A\rightarrow A\rightarrow *) $$

where the carrier is $A$, the base is $x$ and the edge relation is $R$. What's a bit counter-intuitive is that sets are not necessarily well-founded. To get sane notions of equality and membership, we need to define equality as bisimilarity $\simeq$ of pointed graphs.

Then it's pretty easy to define membership: $S\in T$ if

  • $T = (A, x, R)$
  • There is some $y$ with $R\ y\ x$ ($y$ is an element of $x$)
  • $S\simeq (A, y, R)$ ($S$ is the "same set" as $y$)

Then we can show:

For each predicate $P:\mathrm{Set}\rightarrow *$ that respects bisimilarity there is a set $$ \{\ x\ |\ P(x)\ \}$$

It's then easy to show that $P(x)=x\notin x$ respects bisimilarity.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ One can construct the type $U := \Pi (X: \Box_2) (X \to X \to \ast) \to X \to \ast$ of the universe and the relation $\mathsf{elt}\colon U \to U \to \ast$ over $U$, and construct arbitrary sets by the axiom schema of separation. By adding $(\Box_3, \Box_2, \Box_2) \in R$ to $\lambda$Z, one has $U \colon \Box_2$, which leads to the inconsistency. $\endgroup$
    – H Koba
    Commented Apr 16, 2016 at 19:20
  • 1
    $\begingroup$ By mapping $* \mapsto *, \Box_1 \mapsto \Box, \Box_2 \mapsto \Box, \Box_3 \mapsto \triangle$, one can show that System U (and hence $\lambda\ast$) is also inconsistent. The product rule $(\triangle, \Box, \Box)$ corresponds to $(\Box_3, \Box_2, \Box_2)$ in $\lambda$Z. $\endgroup$
    – H Koba
    Commented Apr 16, 2016 at 19:23
  • $\begingroup$ I think I understand how this works with * : *, but could you elaborate how this works in System U? I'm assuming that the construction of {x | P x} relies on instantiating A : * with Set itself somehow? Is that not disallowed in System U, since Set : □ and not Set : *? Or do we have A : □ but still R : A -> A -> *? $\endgroup$
    – Jules
    Commented Sep 20, 2019 at 14:39
  • $\begingroup$ @Jules: $\mathrm{Set}$ has type $*$, just like in system F, $\Pi A:*.A$ has type $*$. This is the impredicative nature of system F, which is even more pronounced in system U, since $\Sigma$ types can be expressed. It's surprising that system F is consistent! $\endgroup$
    – cody
    Commented Sep 21, 2019 at 20:23
  • $\begingroup$ I was worried about the ∗ at the end of R : A -> A -> ∗. What about that one? Doesn't this make Set : □, which means that you can't instantiate A with Set? $\endgroup$
    – Jules
    Commented Sep 23, 2019 at 9:33

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .