What's “conservativity” in terms of type theory and how is it useful?

Question

I have heard that an extension to a type theory can be said to be conservative, which means it may add new formulae to the original type theory, for example new type formers and their intro/elim rules and equations, but the original type theory is left untouched in a sense that we do not create new inhabitants to existing types.

So here are my questions. I tried to approach the idea, but wikipedia defines conservative extension in terms of 'theory', not type theory. A (modern) type theory talks about not just theorems, but also data (like computation of mathematical objects, like numbers) using types, so:

• If an extension adds new inhabitants to a data type instead of a proposition, is it considered conservative?
• If an extension adds new inhabitants to an inhabited type, is it considered conservative?

Also, what does conservativity tell us about the extension? We usually say normalization tells us the decidability of type checking (and much more), canonicity tells us the type theory is a programming language (citation needed), etc., but what about conservativity?

Answer 1

Anja Petković Komel in her PhD thesis Meta-analysis of type theories with an application to the design of formal proofs studied transformations of type theories among other things.

Definition 9.3.3 on page 66 gives the notion of a conservative transformation. This is more general than a conservative extension, which is a conservative inclusion.

Let me give a quick summary. To understand the general definition, we need to know what a boundary is. Every type-theoretic judgement has a boundary and a head:

• the boundary of $\Gamma \vdash A \; \mathsf{type}$ is $\Gamma \vdash \Box \; \mathsf{type}$ and $A$ is the head.
• the boundary of $\Gamma \vdash t : A$ is $\Gamma \vdash \Box : A$ and $t$ is the head.
• the boundary of $\Gamma \vdash A \equiv B$ looks the same as the judgement itself because its head is trivial (judgemental equality is proof irrelevant), but we might write the judgement as $\Gamma \vdash A \equiv B \;\mathsf{by}\; \star$, the boundary as $\Gamma \vdash A \equiv B \;\mathsf{by}\; \Box$ and take $\star$ to be a trivial token that serves as the head.
• similarly for $\Gamma \vdash t \equiv s : A$.

A boundary $\Gamma \vdash \mathscr{b}$ may be filled with a head $e$ to give a judgement $\Gamma \vdash \mathscr{b}\boxed{e}$. For example, filling the boundary $\Gamma \vdash \Box : A$ with $t$ produces $\Gamma \vdash t : A$.

Boundaries are an important concept that is often left implicit, but they deserve to treated properly. For example, a goal in a proof assistant is precisely a well-formed boundary. The goal is solved when its head is filled to give a derivable judgement.

Given a type-theoretic transformation $f : \mathcal{T} \to \mathcal{U}$, we say that $f$ is conservative when the following holds: for any well-formed boundary $\Gamma \vdash_\mathcal{T} \mathscr{b}$ in $T$, if the boundary $f \Gamma \vdash_\mathcal{U} f \mathscr{b}$ can be filled with some $e$ to give a derivable judgement $f \Gamma \vdash_\mathcal{U} (f \mathscr{b})\boxed{e}$, then there is $e'$ such that $\Gamma \vdash_\mathcal{T} \mathscr{b}\boxed{e'}$.

Concretely, suppose $f : \mathcal{T} \to \mathcal{U}$ is an inclusion so that $f(e) = e$. Then conservativity of $f$ amounts to: if $\Gamma \vdash_\mathcal{T} \mathscr{b}$ is well-formed in $\mathcal{T}$ and $\Gamma \vdash_\mathcal{U} \mathscr{b}\boxed{e}$ is derivable in $\mathcal{U}$, then there is $e'$ in $\mathcal{T}$ such that $\mathcal{T}$ derives $\Gamma \vdash_\mathcal{T} \mathscr{b}\boxed{e'}$. In particular, when we specialize this condition to term judgements and term equations, we get:

• if $\Gamma \vdash_\mathcal{T} A \; \mathsf{type}$ and $\Gamma \vdash_\mathcal{U} e : A$ then there is $e'$ such that $\Gamma \vdash_\mathcal{T} e' : A$
• if $\Gamma \vdash_\mathcal{T} s : A$ and $\Gamma \vdash_\mathcal{T} t : A$ and $\Gamma \vdash_\mathcal{U} s \equiv t : A$ then $\Gamma \vdash_\mathcal{T} s \equiv t : A$

You should not take the above as precise definitions, because I skipped over the treatment of meta-variables, which matters. The details are in Petković Komel's dissertation. She also gives examples of conservative transformations, such as definitional extension.

The concept of a conservative transformation subsumes the usual notions of conservativity that one sees in logic books, because first-order theories are special cases of type theories.

Let us apply the concept to your specific question: if an extension adds a new element to a type, is it conservative? Concretely, suppose we have a type $A$ in theory $\mathcal{T}$ to which we add a new constant $\vdash c : A$ to obtain an extended theory $\mathcal{T}'$. If $A$ was empty beforehand, then this is not conservative, consider the boundary $\vdash \Box : A$. Otherwise, consider a closed term $t : A$ and define a further extension $\mathcal{T}''$ which, in addition to $\vdash c : A$, also has the equation $\vdash c \equiv t : A$. Example 9.3.5 of Petković Komel's thesis shows that $\mathcal{T}''$ is a conservative extension of $\mathcal{T}$. We thus have a chain of extensions $$\mathcal{T} \to \mathcal{T}' \to \mathcal{T}''$$ which can be used to show that $\mathcal{T}'$ is a conservative extension: given a boundary $$\Gamma \vdash_\mathcal{T} \mathscr{b}$$ and a filling $$\Gamma \vdash_{\mathcal{T}'} \mathscr{b}\boxed{e},$$ we also get $$\Gamma \vdash_{\mathcal{T}''} \mathscr{b}\boxed{e},$$ and hence by conservativity of $\mathcal{T}''$ over $\mathcal{T}$ we find $e'$ such that $$\Gamma \vdash_{\mathcal{T}} \mathscr{b}\boxed{e'}.$$ Working through Example 9.3.5 tells us how $e'$ is related to $e$: we just replace all occurrences of $c$ with $t$, as one would expect of a definitional extension.

The wheels are turning, the mechanism works.

You asked how the concept is useful. In chapter 10 of the dissertation, a general elaboration theorem is proved: every finitary type theory can be elaborated to a standard type theory. Conservativity plays a role in this theorem: the fact that the retrogression map (the opposite of elaboration) is conservative means that the elaboration does not reconstruct information that is not really there.

Conservativity also plays a role in the design of PAs. Suppose we use an SMT solver $S$ to solve goals in a proof assistant $P$. The situation amounts to a transformation $f : P \to S$ that converts boundaries in $P$ to boundaries in $S$. To say that $f$ is conservative means that it is safe to use the solver $S$: for if $S$ manages to fill a boundary $f \mathscr{b}$ then we know that the original boundary $\mathscr{b}$ can also be filled in $P$. Of course, we need an explicit way of converting the head that $S$ found back to a head in $P$ – but that is precisely a computable witness of conservativity. And also, note that we need not translate back entire derivations, we only need to be able to reconstruct the head.

Answer 2

In the most general setting, I think of convervativity like this. One has a deduction system $D$. There are a set $S$ of strings (or terms) of symbols that one could possibly construct, and a smaller set $T \subseteq S$ that one can construct. Usually, $D$ is a system to prove theorems, and $S$ is all statements and $T$ is the provable statements (i.e. theorems). But it can be more general. For example:

• $S$ is the first-order statements in the language of arithmetic, and $T$ are the ones provable in Peano Arithemetic.
• $S$ is the universal quantified statements of Arthmetic and $T$ are the ones provable in PA.
• $S$ is all prop terms in Lean, and $T$ are the provable ones.
• $S$ is all type terms in Coq, and $T$ are ones you can directly construct a term for.
• $S$ is all configurations of a chess board using chess pieces, $T$ are the ones you can get to from standard game play. (Silly example to prove my point of how general this is.)

Then one adds something to the deduction system to get $D'$. New axioms, new rules, new elements of the language. So you can prove/derive/construct a larger set of things $T'$ extending $T$. You may also be expanding your language so that your new deduction system is proving/constructing/deriving things from a larger set $S'$ of statements expanding $S$. For example, maybe $S'$ is now all sentences of second order arithmetic and $T'$ are those provable using the standard axioms of SOA (as in reverse mathematics). We say this extension is conservative over $S$ (the original set of sentences) if $T' \cap S = T$, that is you can't derive anything new from the statements $S$ in the old language using the new deduction system $D'$.

However, because in practice there are many things we could be interested in, one usually talks of being conservative over some subset $S$ of the language. For example, maybe some change to type theory changes the types which can be inhabited, but doesn't prove any new Props. So we can say that extension is conservative over the propositions. If you just hear the term "conservative", make sure to understand from context what all the parts $D$, $D'$, $S$, $S'$, $T$, and $T'$ are.

---

I'm less sure about adding new elements to types. First, you have to express this proof theoretically. This is all about symbol manipulation, not about actual sets or models. If you are just showing that a type which had no provable inhabitants now has one, then that would fit into the notion of conservative given above (namely that change to the type theory is not conservative over which types are inhabited). However, if a type already has terms constructed for it, if you are constructing new terms to a type, this could just be because your language is bigger so you have names for more things.

Also, then one should be careful. Even if you can show that you can add a new term which is not equal to any previously constructible term does not mean what you may think it means. For example, you could define the complex numbers as the algebraic closure of the real numbers. Without the axioms of choice, you couldn't specify a term for i (since you can't distinguish from the two second roots of unity). But with an axiom saying that i : complex and i * i = -1, then you can have a term for i, but you aren't really changing anything about the elements in the complex numbers, just which ones have "names".

I wouldn't be surprised that most cases where you are adding elements to a type in a substantial way, that you aren't also adding an element to some previously uninhabited type. But that is just a hunch.

Similarly, one has to be careful since constructing an element of a type directly may be different from the proposition that merely says that an element of that type exists. (Again, this goes back to asking what an extension is conservative over.)

My guess is that "conservative" is not typically used to talk about whether or not you are adding elements to previously inhabited types, but that is mostly because it isn't a well formed idea. On the other hand, I could also imagine it is possible there is some case out there where it makes perfect sense, and if you used the word "conservative" for this case, no one would blink an eye. Again, that is a hunch.

---

Last, I'm not a proof theorist or type theorist and maybe I'm wrong about how general the term "conservative extension" can be taken. See section 3.2 in Definitional Extension in Type Theory for a more conservative :) take on the definition of "conservative extension" as applied to type theory.