17
$\begingroup$

I'm surprised that people keep adding new types in type theories but no one seems to mention a minimal theory (or I can't find it). I thought mathaticians love minimal stuff, don't they?

If I understand correctly, in a type theory with a impredicative Prop, λ-abstraction and Π-types suffice. By saying suffice I mean it could be used as intuitionistic logic. Other types can be defined as following:

$$ \bot \stackrel{def}{=} \Pi \alpha: Prop. \alpha \\ \neg A \stackrel{def}{=} A \to \bot \\ A \land B \stackrel{def}{=} \Pi C: Prop. (A \to B \to C) \to C \\ A \lor B \stackrel{def}{=} \Pi C: Prop. (A \to C) \to (B \to C) \to C \\ \exists_{x: S}(P(x)) \stackrel{def}{=} \Pi \alpha: Prop. (\Pi x: S. P x \to \alpha) \to \alpha \\ $$

My first question is, do they (λ, Π) really suffice? My second question is, what do we need minimally if we don't have an impredicative Prop, such as in MLTT? In MLTT, Church/Scott/whatever encoding doesn't work.

Edit: related

$\endgroup$
  • 2
    $\begingroup$ What would a "minimal" type be resp. which properties would it have, in your opinion? $\endgroup$ – Raphael Mar 16 '16 at 15:15
  • $\begingroup$ Being able to prove what Coq can prove? I admit I don't have a clear answer in my mind D: $\endgroup$ – 盛安安 Mar 16 '16 at 15:30
  • $\begingroup$ But I've heard that Coq added universe polymorphism, which the minimal system I proposed obviously does't work for. What about "Being able to prove what MLTT (in the normal sense) can prove."? I thought W-types can be simulated? Though I haven't wrap my head around it in general. $\endgroup$ – 盛安安 Mar 16 '16 at 15:39
  • $\begingroup$ Wait, it seems that with impredicative Prop we don't even need equality. $\endgroup$ – 盛安安 Mar 16 '16 at 16:40
12
$\begingroup$

To elaborate on gallais' clarifications, a type theory with impredicative Prop, and dependent types, can be seen as some subsystem of the calculus of constructions, typically close to Church's type theory. The relationship between Church's type theory and the CoC is not that simple, but has been explored, notably by Geuvers excellent article.

For most purposes, though, the systems can be seen as equivalent. Then indeed, you can get by with very little, in particular if you're not interested in classical logic, then the only thing you really need is an axiom of infinity: it's not provable in CoC that any types have more than 1 element! But with just an axiom expressing that some type is infinite, say a natural numbers type with the induction principle and the axiom $0\neq 1$, you can get pretty far: most of undergraduate mathematics can be formalized in this system (sort of, it's tough to do some things without the excluded middle).

Without impredicative Prop, you need a bit more work. As noted in the comments, an extensional system (a system with functional extensionality in the equality relation) can get by with just $\Sigma$ and $\Pi$-types, $\mathrm{Bool}$, the empty and unit types $\bot$ and $\top$, and W-types. In the intensional setting that's not possible: you need many more inductives. Note that to build useful W-types, you need to be able to build types by elimination over $\mathrm{Bool}$ like so:

$$ \mathrm{if}\ b\ \mathrm{then}\ \top\ \mathrm{else}\ \bot $$

To do meta-mathematics you'll probably need at least one universe (say, to build a model of Heyting Arithmetic).

All this seems like a lot, and it's tempting to look for a simpler system which doesn't have the crazy impredicativity of CoC, but is still relatively easy to write down in a few rules. One recent attempt to do so is the $\Pi\Sigma$ system described by Altenkirch et al. It's not entirely satisfying, since the positivity checking required for consistency isn't a part of the system "as is". The meta-theory still needs to be fleshed out as well.

A useful overview is the article Is ZF a hack? by Freek Wiedijk, which actually compares the hard numbers on all these systems (number of rules and axioms).

$\endgroup$
  • $\begingroup$ Are $\Sigma$-types definable in ETT? $\endgroup$ – 盛安安 Oct 1 '16 at 16:51
  • $\begingroup$ Actually no, I believe you need to assume those as well. My mistake. $\endgroup$ – cody Oct 2 '16 at 2:26
11
$\begingroup$

The problem with Church encodings is that you cannot obtain induction principles for your types meaning that they are pretty much useless when it comes to proving statements about them.

In terms of minimality of the system, one path mentioned in the comments is to use containers and (W / M)-types however they are rather extensional so that's not really convenient to work with in systems like Coq or Agda.

A more tractable approach is to use a polynomial functor defined as the extension of a Description rather than as the one of a container. The host theory only needs to be closed under $\Pi$, $\Sigma$ and $\mu$ and $\nu$ fixpoints (and equality for indexed polynomial functors). You get the same expressive power as with a (W / M)-type without the inconvenients: one can actually prove an induction principle without needing functional extensionality.

Nested fixpoints are more cumbersome but can be dealt with. I haven't written or seen a fully worked-out story about alternating $\mu$s and $\nu$s but it ought to exist.

$\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.