Re: [isabelle] Full vs Henkin Semantics



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> 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
> 





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