15
$\begingroup$

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?)

$\endgroup$
3
  • 2
    $\begingroup$ I've fixed what I assumed is a typo, replacing "infinite cardinals" with "inaccessible cardinals". I will also remark that actually the theory is ZFC+"there are n inaccessible cardinals" for all n - this is subtly different from ZFC+"there are n inaccessible cardinals for all n", as the former theory doesn't prove there are infinitely many inaccessibles while the latter does. $\endgroup$
    – Wojowu
    Mar 2 at 20:54
  • 2
    $\begingroup$ I just realized that there is a possible misnomer here: you are not talking about the "meta-theories" but of the "underlying theories". The "meta-theory of a proof assistsnt" would be a theory in which we prove things about the proof assistant. May I change the title and the text? $\endgroup$ Mar 3 at 20:20
  • 1
    $\begingroup$ @Wojowu: What precisely does "ZFC + countably many inaccessible cardinals" mean? Lean's type theory cannot establish the existence of infinitely many cardinals, but for each $n \in \mathbb{N}$ it can prove that there are $n$ universes. $\endgroup$ Mar 3 at 20:22

3 Answers 3

17
$\begingroup$

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".

$\endgroup$
3
  • 3
    $\begingroup$ This looks like a bona fide answer to me. It clearly outlines the issues involved and the multi-dimensionality of the problem. $\endgroup$ Mar 2 at 14:59
  • $\begingroup$ It's worth noting that "progress + SR + SN" is much stronger than consistency, so not an orthogonal consideration. $\endgroup$
    – cody
    Mar 2 at 22:55
  • 2
    $\begingroup$ @cody it depends how you define progress. If your type-theory happens to be effectful, the progress lemma may tell you that the term might perform effects when reducing. For instance, the Exceptional Type Theory validates all three criteria but is inconsistent. $\endgroup$ Mar 3 at 7:25
11
$\begingroup$

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:

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.

$\endgroup$
4
  • 1
    $\begingroup$ The standard trick to make Prop work is to use the so-called Aczel trace encoding of functions. This is not a problem since ZFC comes in kit form and functions are not even built-in. Otherwise, I am not sure you can exploit the isomorphism without a strongly annotated theory, which will cause more issues with cumulativity and the like. $\endgroup$ Mar 2 at 15:13
  • $\begingroup$ Do you mean n-fold products rather than coproducts for contexts? $\endgroup$ Mar 2 at 19:30
  • 1
    $\begingroup$ I don't want to call those products. If anything, they're dependent sums. But I agree "coproduct" is unsuitable, I changed it to dependent sum. $\endgroup$ Mar 2 at 19:41
  • $\begingroup$ I was not aware of Aczel's trace encoding, thanks! I will incorporate your suggestion into my answer. And the paper you linked to is precisely the sort of reference I was hoping to get. $\endgroup$ Mar 2 at 19:47
6
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.