I enjoy reading about formal logic as an occasional hobby. However, one thing keeps tripping me up: I seem unable to understand what's being referred to when the word "type" (as in type theory) is mentioned.
Now, I understand what types are in programming, and sometimes I get the impression that types in logic are just the same thing as that: we want to set our formal systems up so that you can't add an integer to a proposition (for example), and types are the formal mechanism to specify this. Indeed, the Wikipedia page for type theory pretty much says this explicitly in the lead section.
However, it also goes on to imply that types are much more powerful than that. Overall, from everything I've read, I get the idea that types are:
- like types in programming
- something that is like a set but different in certain ways
- something that can prevent paradoxes
- the sort of thing that could replace set theory in the foundations of mathematics
- something that is not just analogous to the notion of a proposition but can be thought of as the same thing ("propositions as types")
- a concept that is really, really deep, and closely related to higher category theory
The problem is that I have trouble reconciling these things. Types in programming seem to me quite simple, practical things (alhough the type system for any given programming language can be quite complicated and interesting). But in type theory it seems that somehow the types are the language, or that they are responsible for its expressive power in a much deeper way than is the case in programming.
So I suppose my question is, for someone who understands types in (say) Haskell or C++, and who also understands first-order logic and axiomatic set theory and so on, how can I get from these concepts to the concept of type theory in formal logic? What precisely is a type in type theory, and what is the relationship between types in formal mathematics and types in computer science?
(I am not looking for a formal definition of a type so much as the core idea behind it. I can find several formal definitions, but I've found they don't really help me to understand the underlying concept, partly because they are necessarily tied to the specifics of a particular type theory. If I can understand the motivation better it should make it easier to follow the definitions.)