Re: [isabelle] Full vs Henkin Semantics



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

On Wed, Jun 3, 2015 at 11:49 AM, Larry Paulson <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> 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.