Email Gateway (Aug 22 2022 at 17:49): Email Gateway (Aug 22 2022 at 17:49):From: Ken Kubota <mail@kenkubota.de>
Not quite a correction, but an important addendum to the last part ("Legacy") is type abstraction, which Mike Gordon suggested for HOL (but didn't implement), shaping future research. He already foresaw a binding of variables connecting both term and type (subscript) level. (Gordon positively refers to Tom Melham's extension of HOL [Gordon, 2000, p. 175, fn. 7]. R0 incorporates type abstraction as a standard feature.)
Mike Gordon suggesting type abstraction for HOL: “The syntax and semantics of type variables are currently being studied by several logicians. A closely related area is the theory of ‘second order’ λ-terms like λα. λx:α. x, perhaps such terms should be included in the HOL logic.” [Gordon, 2001, p. 22]
http://www.owlofminerva.net/files/fom.pdf <http://www.owlofminerva.net/files/fom.pdf>, p. 7
Besides this, the article is excellent.
I was astonished that it even mentions the awareness of social class distinctions (white vs. brown coats), as in
http://www.cl.cam.ac.uk/archive/mjcg/plans/NorthThamesGasBoard.html#white-versus-brown-coats <http://www.cl.cam.ac.uk/archive/mjcg/plans/NorthThamesGasBoard.html#white-versus-brown-coats>
https://arxiv.org/pdf/1806.04002.pdf <https://arxiv.org/pdf/1806.04002.pdf>, p. 2
Ken Kubota
Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>
Last updated: Apr 18 2024 at 20:16 UTC