Email Gateway (Aug 19 2022 at 15:57): Email Gateway (Aug 19 2022 at 15:57):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all,
I'm not playing with Isabelle since some time, but still read from time to
time on things around it: type theory and proof theory and HOL. I came to
a question related to HOL and type theory, and though this may be the best
place to ask for, due to Isabelle being very close to it.
I landed onto this paper:
http://www.cs.ru.nl/~herman/PUBS/inconsist-hol.pdf
In the abstract, it says “HOL, or its type theoretic variant λHOL”. Does
that mean the real name of HOL with simple type theory is λHOL? And also,
does that mean there exist(ed) an HOL outside any type theory? (for the
latter, I don't see how, but may be I'm too much biased on this). Or I am
misunderstanding this sentence?
With thanks, and have a nice day.
Email Gateway (Aug 19 2022 at 15:58):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I guess I found an answer here,
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers_sl3.pdf
, and the answer is yes.
Email Gateway (Aug 19 2022 at 15:58):From: Yannick <yannick_duchene@yahoo.fr>
An attempt to draw a picture of what various meanings of HOL may be, was
already made in a prior thread in this news‑group (last year, I believe),
and it's indeed rather large, especially for a
non‑student/non‑professional.
What I understand from the second paper, is that the “λ” in “λHOL” denotes
a reference to the location of the named theory on the lambada‑cube
(something I already heard about before).
I had this question wondering if it's something new I did not knew or a
new name for something I already knew. To tell more, my guess is: HOL is a
friendly name, and λHOL is a more formal name with a reference to the
lambda‑cube, so not a new logic (if I'm not wrong).
With thanks for your concern
Last updated: Apr 20 2024 at 12:26 UTC