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.
> 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 ?
> If it is full semantics, are there any automated theorem provers based
> on Henkin semantics for higher-order or secord-order logic?
>  http://en.wikipedia.org/wiki/Higher-order_logic
This archive was generated by a fusion of
Pipermail (Mailman edition) and