[Rseend: I got no response first time round]
On Thursday 25 Sep 2008 10:28 pm, Peter Vincent Homeier wrote:
Since I began using HOL88 many years ago, I have always heard that the
logic of HOL was higher order logic,
...
However, when reading both of these, I see that in neither case does the
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 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
I'm not sure if this is of interest to readers of this thread, but here
goes:
Elements of Functional Programming, by Chris Reade (a student level
textbook) has this to say, at pp 396-7:
(talking about type inference)
(quote)
Note that in these inferences, we used T, T-1, ..., as meta type
On Thursday 25 Sep 2008 10:28 pm, Peter Vincent Homeier wrote:
Since I began using HOL88 many years ago, I have always heard that the
logic of HOL was higher order logic,
...
However, when reading both of these, I see that in neither case does the
type system proposed contain type variables
