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.
Asked By : 盛安安
Answered By : cody
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).
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/54548
0 comments:
Post a Comment
Let us know your responses and feedback