This prompted me to go back and check Andrews' book "An Introduction to Mathematical Logic and Type Theory:To Truth Through Proof". In there, he presents Q_0, which does not have object language type variables. Variables in the meta language are used instead. I wonder why he decided not to use the Q from his thesis ...
Konrad. On Oct 9, 2008, at 10:03 AM, Tom Melham wrote: > Rob, Peter: > > Peter Andrews' PhD thesis, supervised by Church and published by > North-Holland in 1965, describes a simple type theory called "Q" that > definitely includes object-language type variables. In fact Q also > includes > object-language universal quantification over these variables. > > Tom > ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
