2020-03-26 9:2:58 (GMT)
Jasmin insists that we use standard HOL for our HO superposition calculus. That sounds like a good idea, but is there such a thing as standard HOL (with Henkin semantics)? And where can I find a description of it?
2020-03-26 9:4:43 (GMT)
Hm :)
2020-03-26 9:5:7 (GMT)
Peter Andrews is pretty standard for the syntax of HOL and the standard semantics.
2020-03-26 9:5:31 (GMT)
I don't remember whether he had much to say about Henkin semantics, though.
2020-03-26 9:5:40 (GMT)
And my book lies on my desk in A'dam IIRC.
2020-03-26 9:6:13 (GMT)
He has slightly weird notations and typesetting, but his definition of Q_0 (a.k.a. HOL) is good.
2020-03-26 9:6:19 (GMT)
You could ask Ken Kubota.
2020-03-26 9:7:16 (GMT)
He's a bit on the esotheric side of things, but he has a broad knowledge of the literature around HOL and has written some summaries somewhere. Let me look.
2020-03-26 9:10:5 (GMT)
Oh, I had no idea that he was based in RLP:
https://kenkubota.de
2020-03-26 9:13:18 (GMT)
I found this survey:
2020-03-26 9:13:51 (GMT)
Since you also have polymorphism, I doubt you'll find something that works out of the box with Henkin semantics.
2020-03-26 9:14:20 (GMT)
The HOL documentation's Logic manual is definitely standard semantics only.
2020-03-26 9:46:5 (GMT)
Andrews does not seem to define Henkin semantics in his book.
2020-03-26 9:46:30 (GMT)
I found this paper: http://page.mi.fu-berlin.de/cbenzmueller/papers/J6.pdf
2020-03-26 9:47:8 (GMT)
My current approach is to follow Fitting, but there are quite a few things that I adapted.
2020-03-26 10:15:58 (GMT)
I wrote to Ken, but probably following Fitting is not such a bad idea. It's just that his logic
2020-03-26 10:25:53 (GMT)
Ah, I didn't have J6.pdf on my radar.
2020-03-26 10:26:17 (GMT)
I think it's what guided them in the early days of the TPTP (see Benz. & Brown TPHOLs 2005 paper).
2020-03-26 10:26:28 (GMT)
Before the HO problems were part of the TPTP, actually.
2020-03-26 10:46:15 (GMT)
Benzmüller, Miller: Automation of Higher-Order Logic ( https://www.lix.polytechnique.fr/~dale/papers/automationHOL.pdf ) might also contain some pointers.
2020-03-26 11:10:39 (GMT)
Thanks Martin, this pointed back to Andrews, which made me have a closer look. Andrews does not call it Henkin semantics, but general models. But they are defined in his book "To truth through proof".
2020-03-26 11:10:47 (GMT)
So I suppose that is the standard?
2020-03-26 11:14:29 (GMT)
It's a bit different from Fitting, but I suppose I can make it work.
2020-03-26 11:29:30 (GMT)
Afaik, Andrews goes further and defines all logical operators via equality (chapter 51) which also reflects in the semantics (chapter 54). I think most people stay on the level of what Andrews calls system Fω (chapter 5) though.