*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem*From*: Makarius <makarius at sketis.net>*Date*: Sat, 21 Jul 2012 20:44:54 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <500986C6.6060905@gmx.com>*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> <500986C6.6060905@gmx.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 20 Jul 2012, Gottfried Barrow wrote:

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.Because I read things that I don't completely understand that make meworry, such as that certain things can be proved about FOL that can't beproved about HOL. Was that "completeness" that I read about? I don'teven look it up.

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.Here, I don't even know what "weaker" means because I've found no standarddefinition anywhere for "logically weaker".However, I've found enough information to assume that it means thateverything you can prove with HOL can be proved with FOL+ZF, but notvice versa.

Makarius

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

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

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] Automating the auto-tools
- 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