What is known about the consistency of proof assistant metatheories?

Question

I realised I don't know the status of consistency of theorem provers' metatheories - what is currently known? For example, as far as I know Lean's type theory is equiconsistent to ZFC+countably many inaccessible cardinals; however, I've heard contradictory statements about Coq, with some claims that cumulativity makes this more difficult to prove. Are most commonly used proof-assistants proven to be consistent? Is there any proof assistants whose consistency proofs have been formalized (either in the same system or in another?)

Answer 1

This is more of a comment than an answer. I really look forward to the answers, but it should be noted that there are a lot of subtleties when saying that a system is consistent.

First, a logical kernel is built around a core logical theory, like CiC, HOL, etc. It is likely that there is at least some version of that theory which is known to be consistent (relative to some established meta-theory like ZFC + omega large cardinals). However, actual kernels add on top of that theory many features. Ideally, all features and implementation details in the kernel need to be addressed for a full proof of consistency. (Mario does this with Lean in his thesis for example.)

Also, the rules and axioms used in practice for a proof assistant may not be limited to what is found in the logical core or the standard library. For example, in Coq, the core is very minimalist, but different libraries also introduce their own axioms (to say use quotients similar to those in Lean). Ideally we should keep track of which combinations of axioms and features are known to be consistent. (And maybe which combinations of libraries are known to be consistent.) An extreme example of this is Metamath, even with the common set.mm database. My understanding is that in some sense every definition in Metamath is an axiom. Nonetheless, it is known that if the definition is of a certain form, then it doesn't effect consistency.

It is also known in some rare cases that people make experimental provers or add experimental features where it is possible to do something inconsistent but also they know how to avoid it. type : type comes in mind, but I think there have been other real world examples.

Of course, a logic which is consistent on paper, may not be consistent in practice, due to implementation bugs (there were two variable bugs found over time in the HOL-Light kernel for example). To address this, there have been projects formally verifying the kernel. I see two dimensions to projects like this.

• The first dimension is if you formally verify the actual kernel with all features and implementation details (and the actual code for the kernel), or if you just verify a formal model of the kernel possibly leaving out many details.
• The second dimension is if you verify that the kernel follows the rules of the logic (this is the goal of say Metamath Zero), or you verify that the logic is consistent (relative to some axioms like large cardinals).

Also, most proofs of consistency, even the formal ones, probably assume some trust that the user isn't an adversarial hacker. For example, since HOL-Light tactics are just OCaml functions, one could in theory write a tactic to mess with the machine memory. (I'm not that proficient in this stuff, so I don't know if this will actually work.) Similarly, one could theoretically write a Lean tactic with tactic.unsafe_run_io which can access your command line, and from there, mess with your machine. (Again, I don't mean to scare anyone here. It is just an intellectual curiosity.)

Finally, not everyone thinks consistency should be the main goal. For example, ppedot thinks that type-theoretic properties like "progress, strong normalization, subject reduction and decidability of type-checking" are more important. Conversely, digama0 thinks the most important thing is "soundness relative to the model that we carry around in our heads".

Answer 2

I am not familiar enough with the literature on this question to be able to point to specific papers, but allow me to make a basic sketch on how one can set up set-theoretic models of type theories. I am not addressing consistency of the actual implementations, but only of the underlying formalisms.

Supplemental: I shall collect here useful references:

• Gyesik Lee, Benjamin Werner: Proof-irrelevant model of CC with predicative induction and judgmental equality – a set-theoretic model of the Calculus of Inductive Constructions. (This paper subsumes much if not all of what is written below. I recommend it. Thanks to Pierre-Marie Pédrot for citing it in the comments.)

The ideas presented below are fairly simple and work whenever we have a theory that is consistent with classical set theory. Coq, Agda, Lean, HOL and Mizar are all of this kind, as they do not actively postulate any anti-classical axioms.

Types are interpreted as sets. $\newcommand{\sem}[1]{[\![#1]\!]}$

Contexts are interpreted as sets. The context $$x_1 : A_1, \ldots, x_n : A_n$$ is interpreted as an $n$-fold dependent sum (a telescope) whose underlying set is $$\big\{(a_1, \ldots, a_n) \mid a_1 \in \sem{A_1}, a_2 \in \sem{A_2}(a_1), \ldots, a_n \in \sem{A_n}(a_1, \ldots, a_{n-1}) \big\}.$$ Dependent types are interpreted as families of sets. That is, a type $\Gamma \vdash A \; \mathsf{type}$ is interpreted as a function $\sem{A} : \sem{\Gamma} \to \mathsf{Set}$ where $\mathsf{Set}$ is the class of all sets (by replacement such a function is represented by a set-sized graph). Next, we interpet dependent sums and products as coproducts and products of families, respectively.

Various kinds of inductive types can be constructed using known methods. In many cases, the signature for an inductive type induces a covariant accessible functor $F : \mathsf{Set} \to \mathsf{Set}$, and such functors have well-behaved initial algebras, which serve as denotations of inductive types. This is all fairly well known (and I ask here for help from knowledgable people to suggest reading material).

Induction-recursion is trickier because it is known to require large cardinals, so let us leave that as an “advanced topics”. It touches upon fancy stuff like Mahlo cardinals.

Next we come to universes. Recall that for $\kappa$ a strongly inaccessible cardinal $\kappa$ the set $V_\kappa$ in the cumulative hierachy is a model of ZFC. Therefore, $V_\kappa$ is itself a model of type theory closed under dependent sums and products, as well as sufficiently tame kinds of inductive types. Moreover, if $\kappa < \lambda$ then both $V_\kappa \in V_\lambda$ and $V_\kappa \subseteq V_\lambda$. It's not called a cumulative hierachy for nothing.

Universes are interpreted as sets $V_\kappa$ for inaccessible $\kappa$. We automatically get cumulativity by the previous remark. Concretely, suppose we want to model Russell-style cumulative universes $U_0, U_1, U_2, \ldots$. We sell a couple of souls to the devil for a countable chain of inaccessible cardinals $\kappa_0 < \kappa_1 < \kappa_2 < \cdots$ and set $$\sem{U_i} = V_{\kappa_i}.$$ This works because the elements of $V_{\kappa_i}$ are sets, which are denotations of types.

Tarski-style universes are just as easy, because we can reuse the same interpretation and observe that the decoding function is the identity.

What about non-cumulative hierarchies? We can reuse the same idea and interpret liftings $U_i \to U_j$ as inclusions $V_{\kappa_i} \subseteq V_{\kappa_j}$.

Let us apply the above ideas to outline a set-theoretic model of Coq. It has a cumulative hierarchy of Russell-style universes $$\mathsf{Prop}, \mathsf{SProp}, \mathsf{Set}, \mathsf{Type}_1, \mathsf{Type}_2, \ldots$$ subject to the following constraints:

1. $\mathsf{Prop} : \mathsf{Type}_1$ and $\mathsf{SProp} : \mathsf{Type}_1$ and $\mathsf{Set} : \mathsf{Type}_1$,

2. $\mathsf{Type}_i : \mathsf{Type}_{i+1}$ for all $i \geq 1$,

3. Cumulativity:

   • if $e : \mathsf{Type}_i$ then $e : \mathsf{Type}_{i+1}$,
   • if $e : \mathcal{S}$ where $S \in \{\mathsf{Prop}, \mathsf{SProp}, \mathsf{Set}\}$ then $e : \mathsf{Type}_1$.

4. Impredicativity: $\mathsf{Prop}$ is closed under dependent products indexed by any type.

(I hope I am getting these right, but even if not, it should be possible to accommodate a slightly different arrangement.)

The hierarchy is interpreted as follows. Let $\kappa_0 < \kappa_1 < \kappa_2 < \cdots$ be an infinite chain of inaccessible cardinals, and set

\begin{align} \sem{\mathsf{Prop}} = \sem{\mathsf{SProp}} &= \{\emptyset, \{\emptyset\}\},\\ \sem{\mathsf{Set}} &= V_{\kappa_0},\\ \sem{\mathsf{Type}_i} &= V_{\kappa_1}. \end{align}

This satisfies all the cumulativity requirements.

There is a slight problem with impredicativity. Suppose $A : I \to \{\emptyset, \{\emptyset\}\}$ is a family such that $A_i = \{\emptyset\}$ for all $i \in I$. Then we get $$\Pi_{i \in I} A_i = \{ (i \mapsto \emptyset) \}$$ but we really need $$\Pi_{i \in I} A_i = \{ \emptyset \}.$$ We can solve the problem by using a construction by Aczel, see Definition 3.2 in Proof-irrelevant model of CC with predicative induction and judgmental equality by Lee and Werner.

Answer 3

Because HOL is so weak, it has had a quite a bit of work done on its semantics and soundness, both at the logic level, and in terms of implementations. The bibliography in Oskar Abrahamsson’s recent paper, A Verified Proof Checker for Higher-Order Logic links to lots of this, including, for example, Self-formalisation of higher-order logic: semantics, soundness, and a verified implementation by Kumar et al.

The first HOL paper in this vein was probably Harrison, Towards self-verification of HOL Light in IJCAR 2006.