¿Teoría de tipo intuitiva "mínima"?

18

Me sorprende que la gente siga agregando nuevos tipos en las teorías de tipos, pero nadie parece mencionar una teoría mínima (o no puedo encontrarla). Pensé que los matemáticos aman las cosas mínimas, ¿no?

Si entiendo correctamente, en una teoría de tipos con un carácter impredecible Prop, la abstracción λ y los tipos Π son suficientes. Al decir suficiente quiero decir que podría usarse como lógica intuicionista. Otros tipos se pueden definir de la siguiente manera:

=defΠα:Prop.α¬A=defAAB=defΠC:Prop.(ABC)CAB=defΠC:Prop.(AC)(BC)Cx:S(P(x))=defΠα:Prop.(Πx:S.Pxα)α

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

盛安安
fuente
2
What would a "minimal" type be resp. which properties would it have, in your opinion?
Raphael
Being able to prove what Coq can prove? I admit I don't have a clear answer in my mind D:
盛安安
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.
盛安安
Wait, it seems that with impredicative Prop we don't even need equality.
盛安安

Respuestas:

12

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 01, 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 Σ and Π-types, Bool, the empty and unit types and , 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 Bool like so:

if b then  else 

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 ΠΣ 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).

cody
fuente
Are Σ-types definable in ETT?
盛安安
Actually no, I believe you need to assume those as well. My mistake.
cody
11

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 Π, Σ and μ and ν 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 μs and νs but it ought to exist.

gallais
fuente