Re: [isabelle] Full vs Henkin Semantics



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


> On 3 Jun 2015, at 18:24, Konrad Slind <konrad.slind at gmail.com> wrote:
> 
> 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 <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
> 
> On Wed, Jun 3, 2015 at 11:49 AM, Larry Paulson <lp15 at cam.ac.uk <mailto:lp15 at cam.ac.uk>> wrote:
> 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
> 
> 
> > On 3 Jun 2015, at 17:45, Andrew Gacek <andrew.gacek at gmail.com <mailto:andrew.gacek at gmail.com>> wrote:
> >
> > 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 <http://en.wikipedia.org/wiki/Higher-order_logic>
> >
> 
> 
> 




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