*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 11:26:46 -0500*In-reply-to*: <alpine.LNX.2.00.1207201629180.26147@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> <5009674D.9070804@gmx.com> <alpine.LNX.2.00.1207201629180.26147@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 9:34 AM, Makarius wrote:

On Fri, 20 Jul 2012, Gottfried Barrow wrote:Quantifying over functions has me a little worried.Why? Semantically a function is just a set, and in mathematics you qantify over collections of sets all the time.

You can take HOL is a simplified version of FOL + set theory, but with an explicit type system. Paradoxically HOL is weaker that FOL + ZF set theory, despite arbitrary abstraction and quantification in HOL.

> Anyway, in practice you don't need to worry about the foundations and > their relative logical strenth.

You just do your applications with high-level specification mechanims in Isabelle (datatype, function, inductive, locale etc.), better not axiomatization.

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

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