Criterion for the consistency of pure type systems Pure type systems are characterized in an almost combinatorial way: a set of axioms $\star_i : \star_j$, and a set of triples $(\star_i, \star_j, \star_k)$ saying when the dependent product $\prod_{x : A} B(x)$ can be formed and where it goes -- $\prod_{x:A}B(x) : \star_k$ exactly when $A:\star_i, B:\star_j$, ignoring context issues.
So a question arises, so naturally that I was puzzled when I could not find any relevant results: is there some simple criterion to determine when a pure type system is consistent? I don't expect such a criterion to be both sound and complete though, given the logical complexity that lies therein.
Is there any results concerning this question? I'm grateful if you could provide a pointer to them.
 A: I'll write some fragment of thoughts here.
First some known results. All the lambda cube is consistent (and normalizing, though I didn't mention it in the question, I'm also interested in that). A hierarchical structure that $\star_i : \star_{i+1}$ and the rule $(\star_i, \star_j, \star_k)$ only if $k > i, j$ is consistent, by @AndrejBauer 's construction (I came across a webpage detailing that, but I lost the URL, I'll link when I find it). And system $U^-$ is inconsistent, suffering from Girard's paradox.
Next, some graph theoretic reductions. Consider the PTS as a hypergraph with 2- and 3-edges. Then one can just consider the connected components. Also, an embedding $\lambda S_1 \to \lambda S_2$ of two PTS's (i.e. a map of the vertices that preserve the edges) reflects consistency: the consistency of $\lambda S_2$ implies that of $\lambda S_1$, and the reverse implication for inconsistency.
I think there is some way to chop off some wandering edges, but I haven't got into that yet. But the idea is to define a weak dependency between sorts. Say $\star_i$ weakly depends on $\star_j$ if for some expression $\Gamma, x:N \vdash A:M:\star_i$ where $N:\star_j$, $A$ can contain $x$ in a well-typed fashion. If there is no weak dependency, the rule $(\star_i, \star_j, \star_k)$ can probably be translated away by a similar method of translation from $\lambda P$ to $\lambda ^\to$, see Barendregt's Lambda Calculi with Types.
I fancy if we make enough reductions, we might determine the consistency of all PTS's. The hope lies in that most PTS's are probably trivially inconsistent because they are just too entangled and impredicative :(
