Earlier quoted context omitted.
This is what I don't get... _Why_ is 'type' theory _a logic_? A type is an enumeration of values (terms), right? What's that got to do with truth values and how they may be manipulated? I've read some of the papers/texts you posted in that tremendously helpful summary (thanks by the way!) and talking about type theory always segues into talking about logic. If you could explain that _one_ thing I'd be so happy. To me…
Ahh this is a very good question.. I'll give two answers, the first more philosophical and the second more example-driven, and both hesitant, 'cause I'm not sure anyone's really thought about deeper why's like this much. :) 1: My first answer is, because of the nature of what a logic is. Logics are systems for reasoning about some problem domain, or put it another way, logics are ways of convincing yourself that you'…
I would like to continue this conversation with you but here is not the correct space/place. I will join the group on IRC and I hope to catch you there.