Tools for checking the consistency of a type theory

Question

My question is twofold:

• How do you define consistency (analogously to the concept in first-order logic) in the context of a type theory?
• Are there any tools that can check consistency?

---

I have seen a few type theories, such as the systems described in the lambda cube, described using typing rules like the following.

$$ \frac{\Gamma \vdash e_1 : \sigma \to \tau \;\;\text{and}\;\; \Gamma \vdash e_2 : \sigma}{\Gamma \vdash e_1(e_2) : \tau} \;\; \text{is implication elimination in STLC} $$

I have a vague, intuitive sense of what consistency might mean for a type system. I don't know the true definition of consistency here. I'm offering up two examples (that are possibly incoherent) in an attempt to illustrate the concept I am interested in.

I think but am not certain we can define consistency as the existence of two things:

1. inductive translation into the untyped lambda calculus that preserves and reflects the binary relation $=_{\alpha\beta\eta}$.
2. every well-typed term beta-reduces to a value.

Also, and I'm speculating here, I think we could define consistency as having a semantics-preserving transformation into $\mathsf{ZFC}$ for well-typed terms. The well-foundedness of $\mathsf{ZFC}$ would stop us from constructing an infinite loop (assuming function application is defined in the usual set-theoretic way (i.e. functions are sets of Kuratowksi pairs and application is unioning together all the right elements of pairs with a given left element)).

For concreteness, here is application in $\mathsf{ZFC}$. $\pi_1$ and $\pi_2$ are projections out of a Kuratowski pair.

$$ f(x) := \bigcup \{\pi_2(p) : p \in f \land \pi_1(p) = x \} $$

---

I'm also curious if there are any tools that let you express a type theory as its set of typing rules (in some notation) and then either prove that it's consistent or test it experimentally to see what kinds of properties it has.

So, how exactly do you define consistency (or the equivalent concept) for a type system and are there any tools that can check it for you?

Answer 1

One can think of type theory as an algebraic theory on steroids (there is technical merit to this claim). Every algebraic theory has a model, namely the trivial one whose carrier is the singleton. A trivial theory is one whose models are all trivial, including the initial one.

By analogy we would then say that a type theory is algebraically trivial if its syntactic model is trivial. This is equivalent to saying that it proves all judgmental equalities, which is further equivalent to saying that for every type $A$ it proves $x : A, y : A \vdash x \equiv_A y$.

As soon as the type theory has the booleans, or a type that retracts to booleans (such as $\mathbb{N}$), it is algebraically trivial precisely when it proves $\vdash \mathsf{false} \equiv_{\mathsf{Bool}} \mathsf{true}$.

Algebraic triviality can be seen as one possible notion of inconsistency.

Under propositions-as-types view, it is reasonable to declare a type theory to be inconsistent when all of its types are inhabited (all propositions are provable). This is weaker than algebraic triviality.

Supplemental: I forgot to answer the bit about proving consistency. The two common methods are:

1. Exhibit a non-trivial model of the theory.
2. Directly show that there are uninhabited types or unprovable equations.

For the first method we need a good notion of model, and constructing one for a fancy type theory typically requires some assumptions. For example, one can show that Martin-Löf type theory with one universe is consistent by interpreting it in set theory with one inaccessible cardinal.

One way to show consistency directly is to prove a theorem of the form "every well-typed closed term is equal to a normal term" and then to observe that the empty type does not have any closed normal terms. Another possibility is to show that two well-typed equal terms reduce to the same normal form, then observe that $0$ and $1$ are in normal form, therefore cannot be equal.

Answer 2

First you need to define a notion of consistency for your type theory. As Andrej mentioned, a good notion is to try to prove that $\text{true}\neq\text{false} : \text{Bool}$. $\newcommand{\llb}{[\![}\newcommand{\rrb}{]\!]}$

Now, as you mention, the simplest way would be to interpret types as sets in ZFC. The tricky part is to give a meaning to the judgements $$\Gamma\vdash A$$ $$\Gamma\vdash A \equiv B$$ $$\Gamma\vdash t : A$$ $$\Gamma\vdash s \equiv t : A$$ you could for example interpret them as $$\gamma\in\llb\Gamma\rrb\vdash\llb A\rrb(\gamma)\text{ set}$$ $$\gamma\in\llb\Gamma\rrb\vdash \llb A\rrb(\gamma) = \llb B\rrb(\gamma)$$ $$\gamma \in \llb\Gamma\rrb \vdash \llb t\rrb(\gamma) \in \llb A\rrb(\gamma)$$ $$\gamma\in\llb\Gamma\rrb\vdash \llb s\rrb(\gamma) = \llb t\rrb(\gamma)$$ but this could vary depending on how you choose to interpret your base types. In particular, a function type may be interpreted as a set of functions, and an inductive type may be interpreted as a well-founded set. Then you inductively check that each inference rule is validated by the interpretation.

Now, if you happen to interpret the boolean type as the set with two elements and the interpretation of all your rules are valid, then your theory is consistent.