*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Schematic vars or universal bound vars in theorem?*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Sun, 22 Jul 2012 17:19:30 +0900*In-reply-to*: <500B9DC5.4050703@gmx.com>*References*: <5006C3EC.50004@gmx.com> <485EE543-83A4-4296-A6EB-2FCC934E3825@cam.ac.uk> <5006F2E1.3090605@gmx.com> <alpine.LNX.2.00.1207212030180.15809@macbroy21.informatik.tu-muenchen.de> <500B9DC5.4050703@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

On 07/22/2012 03:29 PM, Gottfried Barrow wrote:

On 7/21/2012 1:32 PM, Makarius wrote:On Wed, 18 Jul 2012, Gottfried Barrow wrote:It's my healthy paranoia kicking in here. I'm using axioms, so I'm trying to use everything I know right now to keep from being inconsistent.The best way is not to use axioms then. In mathematics you define new things by using old ones, and then prove the desired properties. Sometimes you work with abstract theories, but that corresponds to a locale or class definition in Isabelle/HOL, not axiomatization.I'll try to make a short sales speech here to spin the pro-axiom side of things. Suppose there are 10 standard axioms for a language of FOL that have held up for many years. Then there's no more risk in using those axioms than there's ever been.

Right, but combining those axioms with others (say those of HOL) is a risk.

Suppose a person implements those axioms on top of Isabelle/HOL with a slight modification, and others build a lot of standard math on top of those axioms, and no inconsistency shows up.

The scenario I just described would be completely beneficial to Isabelle/HOL as a product. What's done as HOL is just HOL, where HOL is obviously very useful. But if HOL is used as a meta-language to implement another standard logic on top of it, in a way that's reasonably pure, which might require axioms to do, then that's something different.

just my 2 cents, chris

**Follow-Ups**:**Re: [isabelle] Schematic vars or universal bound vars in theorem?***From:*Gottfried Barrow

**References**:**[isabelle] Schematic vars or universal bound vars in theorem?***From:*Gottfried Barrow

**Re: [isabelle] Schematic vars or universal bound vars in theorem?***From:*John Wickerson

**Re: [isabelle] Schematic vars or universal bound vars in theorem?***From:*Gottfried Barrow

**Re: [isabelle] Schematic vars or universal bound vars in theorem?***From:*Makarius

**Re: [isabelle] Schematic vars or universal bound vars in theorem?***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] Failing simproc
- Previous by Thread: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Thread: Re: [isabelle] Schematic vars or universal bound vars in 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