On Oct 25, 2010, at 2:10 PM, Andrew Coppin wrote:
Type theory doesn't actually interest me, I just wandered what the
hell all the notation means.
Sorry for the double email.
I recommend "Language , Proof, and Logic", by Barwise and
Etchemendy. It doesn't go into type theory (directly). It is a book
about logic for technical people (it was in use at the Reed College
philosophy department for many years -- maybe it still is). It is
very approachable. The last part of the book is about "advanced"
logic, including model theory, some aspects of forcing (there's a
forcing proof of Lowenheim-Skolem), Godel's theorems (they called
Godel the world's first hacker, with good reason), and some sections
on higher order logics.
It doesn't include all of the notation you asked about. But
understanding the basics will be very helpful, especially if you
understand the underlying concepts. For example, set theory is a
first order logic that can be recast as a second order logic. This is
more-or-less the origin of type theory (types were originally
witnesses to the "level" at which a term is defined -- this will make
sense in context). The paper you asked about has a richer "ontology"
than ZF -- it promotes more things to "named" "kinds" of terms than
plain old ZF. But the promotion is straightforward, and the same
logical rules apply.
You can get it cheap ($1.70 for the cheapest copy) through alibris.com
(I am not too happy with them at the moment, but their prices are
low. Especially if you can wait a few weeks for the book)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
