[System U](https://en.wikipedia.org/wiki/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](https://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf).


One-sorted circular PTS $\lambda\ast$ ($S = \{\ast \}, A=\{\ast\colon \ast\}, R=\{(\ast,\ast)\}$) (Geuvers' [Logics and Type Systems](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.56.7045&rep=rep1&type=pdf), 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.



Easier Girard's paradox in a circular pure type system (PTS)
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](https://www.fing.edu.uy/~amiquel/publis/these.pdf). 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.*](https://www.fing.edu.uy/~amiquel/publis/types04.pdf).


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.


