Email Gateway (Aug 22 2022 at 10:30): Email Gateway (Aug 22 2022 at 10:30):From: Andrew Gacek <andrew.gacek@gmail.com>
Is HOL in Isabelle/HOL based on full semantics or Henkin semantics [1]?
If it is full semantics, are there any automated theorem provers based
on Henkin semantics for higher-order or secord-order logic?
Thanks,
Andrew
[1] http://en.wikipedia.org/wiki/Higher-order_logic
Email Gateway (Aug 22 2022 at 10:30):From: Larry Paulson <lp15@cam.ac.uk>
This is not my area of expertise, but my impression is that Henkin semantics gives you a completeness theorem for the standard formal system. In other words, there is no formal system specific to Henkin semantics and therefore also no theorem provers specifically for it.
Larry Paulson
Email Gateway (Aug 22 2022 at 10:30):From: Konrad Slind <konrad.slind@gmail.com>
I thought that some of the type theory automated provers
were based on formulas with Henkin semantics. E.g.:
https://www.ps.uni-saarland.de/Publications/documents/Brown2012a.pdf
I have always been puzzled about Standard vs. Henkin as well. So many
articles say something to the effect that "Second Order Logic is not a
logic"!
Konrad
Email Gateway (Aug 22 2022 at 10:30):From: Andrei Popescu <a.popescu@mdx.ac.uk>
Hi Andrew,
Is HOL in Isabelle/HOL based on full semantics or Henkin semantics [1]?
I would say that the HOL-based provers, including Isabelle/HOL, can be seen as "based on Henkin semantics" because of what Larry pointed out:
that HOL deduction is sound and complete w.r.t. (a proper notion of) Henkin semantics. The deduction is of course sound for the full-frame semantics.
Another note: As far as I see, what the theorem proving community calls "the HOL logic" is something quite specific, introduced in Mike Gordon's seminal HOL system: classic higher order logic with infinity, choice, rank-1 polymorphism, constant definitions and a "typedef" mechanism for introducing new types by carving out non-empty subsets of existing types. Isabelle/HOL additionally includes overloaded constant definitions (with possible delay and recursion in the overloading process), which form the basis of type classes. A proper notion of Henkin semantics needs to account for all these.
Best,
Andrei
Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.
If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS. There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.
Email Gateway (Aug 22 2022 at 10:30):From: Larry Paulson <lp15@cam.ac.uk>
The remarks in that paper concerning completeness for Henkin models don’t imply that the calculus is different from one that we would use. Proving completeness for standard inference systems is the point of Henkin models.
Larry Paulson
Last updated: Apr 23 2024 at 20:15 UTC