Skip to main content
1 of 2
Trebor
  • 1.3k
  • 6
  • 16

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.

Trebor
  • 1.3k
  • 6
  • 16