3 ms·

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

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, type theory seems like set theory done right...

psygnisfive 12y ago
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're justified in believing a judgment (`A is true`, `B is a proposition`, `C is tasty`). What this means is that, to have a proof `M` which proves a judgment `J`, is to have some piece of data which you can look at. So all proofs are some kind of data, in the same way that all novels and all movies are some kind of data. A harder question is why all data is a kind of proof and that's more subtle. Some people actually want to say they're not, proofs are just a special kind of data, while others want to just say to loosen the notion of proof and proposition. I don't think there's a good answer for this direction. 2: My second answer is, it turns out they couldn't be anything else! Consider the inference rule (written in natural English): if you know A is true and you know B is true then you can conclude A&B is true which tells you when you can make the judgment `A&B is true`. When you use this rule, you have to supply two justifications of the premises `A is true` and `B is true`. That is, you have to provide two pieces of evidence, two proofs, one for each premise. Now consider this description of how to make pairs: if you have M of type A and you have N of type B then you can make (M,N) of type A*B Here we're just describing how pairs are formed: you take two things, and stick them together with a constructor to form a new piece of data. Now I ask you, what are you doing when "proving A&B" if not taking two things (two smaller proofs of `A` and `B`) and sticking them together to form a new piece of data (the proof of `A&B`)? I would argue you're not doing ANYTHING different. The act of proving a conjunction is just the same as the act of making a pair! Now do this for other logical connectives: proving a disjunction is just the same as giving an element of a tagged union proving an implication is just the same as giving a function proving the trivial proposition is just giving a 0-length tuple proving the absurd proposition (which is impossible) is just giving a void-type value (which is impossible) So why are type theories a logic? Well just look! ---- Now, I should say, this connection does not mean that all logics are type theories! Type theory has a very specific view of how inference rules are justified, by appeal to certain principles which turn out to be computational in nature. Why these principles should be so powerful as computational principles, I don't know. It's a mystery. Maybe God is a type theorist? ;p
- igravious 12y ago
  Thank you for taking the time to reply to me. 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.

psygnisfive 12y ago

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're justified in believing a judgment (`A is true`, `B is a proposition`, `C is tasty`). What this means is that, to have a proof `M` which proves a judgment `J`, is to have some piece of data which you can look at. So all proofs are some kind of data, in the same way that all novels and all movies are some kind of data. A harder question is why all data is a kind of proof and that's more subtle. Some people actually want to say they're not, proofs are just a special kind of data, while others want to just say to loosen the notion of proof and proposition. I don't think there's a good answer for this direction. 2: My second answer is, it turns out they couldn't be anything else! Consider the inference rule (written in natural English): if you know A is true and you know B is true then you can conclude A&B is true which tells you when you can make the judgment `A&B is true`. When you use this rule, you have to supply two justifications of the premises `A is true` and `B is true`. That is, you have to provide two pieces of evidence, two proofs, one for each premise. Now consider this description of how to make pairs: if you have M of type A and you have N of type B then you can make (M,N) of type A*B Here we're just describing how pairs are formed: you take two things, and stick them together with a constructor to form a new piece of data. Now I ask you, what are you doing when "proving A&B" if not taking two things (two smaller proofs of `A` and `B`) and sticking them together to form a new piece of data (the proof of `A&B`)? I would argue you're not doing ANYTHING different. The act of proving a conjunction is just the same as the act of making a pair! Now do this for other logical connectives: proving a disjunction is just the same as giving an element of a tagged union proving an implication is just the same as giving a function proving the trivial proposition is just giving a 0-length tuple proving the absurd proposition (which is impossible) is just giving a void-type value (which is impossible) So why are type theories a logic? Well just look! ---- Now, I should say, this connection does not mean that all logics are type theories! Type theory has a very specific view of how inference rules are justified, by appeal to certain principles which turn out to be computational in nature. Why these principles should be so powerful as computational principles, I don't know. It's a mystery. Maybe God is a type theorist? ;p

igravious 12y ago
Thank you for taking the time to reply to me. 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.