*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 20 Jul 2012 09:12:29 -0500*In-reply-to*: <alpine.LNX.2.00.1207201318440.20336@macbroy21.informatik.tu-muenchen.de>*References*: <5008228D.9070306@gmx.com> <500827AE.6020907@gmx.com> <50087706.2030608@gmx.com> <alpine.LNX.2.00.1207201318440.20336@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/20/2012 6:23 AM, Makarius wrote:

Axiomatizations are very difficult to get right. Experts usually avoid them altogether, and use definitions exclusively. Definitions can be as diverse as 'definition', 'inductive', 'function', 'locale', ...

Lambda calculus is just notations for mathematical functions; '=' is plain classical equality on arbitrary mathematical entities, including functions. HOL is more simple than FOL, because it does not impose any restrictions about quantification and equality. Types in HOL are just separate syntactic domains, which are always non-empty by construction of the logic. This is like the implicit (single) domain of discourse in FOL, but HOL allows many of them, also constructors to operate on such domains: nat, nat => bool, nat set, nat list, ..., 'a * 'b, ...

I head down the road semi-blind, and find out where it leads. Regards, GB

**Follow-Ups**:

**References**:**[isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Gottfried Barrow

**Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem***From:*Makarius

- Previous by Date: Re: [isabelle] Failing simproc
- Next by Date: Re: [isabelle] provers used by sledgehammer
- Previous by Thread: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- Next by Thread: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list