[Haskell-cafe] In what language...?

[Alexander Solla]

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)