7
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • $\begingroup$ What notion of consistency do you have in mind? Note that a pure type system has other structure, apart from dependent products. If you are just asking about the pure pure type system which has only products, then they're all going to be consistent (for any reasonable notion of consistency): just interpret all $\star_i$ as the class of finite sets. $\endgroup$
    – Andrej Bauer
    Commented May 30, 2021 at 9:06
  • 1
    $\begingroup$ @AndrejBauer That interpretation doesn't satisfy $\star_i : \star_j$. $\endgroup$
    – Mike Shulman
    Commented May 30, 2021 at 17:09
  • 1
    $\begingroup$ Good point. I'll have to try harder. How about $\star_i = V_{\kappa_i}$ where $\kappa_i$ is the $i$-th inacccessible cardinal? Do we really need so many inaccessibles, though? $\endgroup$
    – Andrej Bauer
    Commented May 30, 2021 at 18:32
  • 2
    $\begingroup$ @AndrejBauer The subscripts don't imply any order, they are just grabbed from some old indexing set. So, for instance, system U is inconsistent. But your idea actually applies to a huge lot of PTS's. $\endgroup$
    – Trebor
    Commented Jun 9, 2021 at 12:10
  • $\begingroup$ @AndrejBauer We kind of need that many inaccessibles, at least constructively, since there is $\mathrm{CoC}_\omega$ which is as strong as Intuitionistic Zermelo set theory with $\omega$ (Zermelo) universes. $\endgroup$
    – cody
    Commented Dec 1, 2022 at 18:35

1 Answer 1

Reset to default
1
$\begingroup$

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 :(

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ We've written a whole paper on "edge chopping": andrew.cmu.edu/user/fpv/papers/struct_pts.pdf! Note that we talk about termination and not consistency though, since the latter notion is less clear outside of "logical" pure type systems. $\endgroup$
    – cody
    Commented Dec 1, 2022 at 18:37

You must log in to answer this question.

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