Re: [isabelle] Full vs Henkin Semantics



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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.