*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Schematic vars or universal bound vars in theorem?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Sun, 22 Jul 2012 10:57:29 -0500*In-reply-to*: <500BB792.9020401@jaist.ac.jp>*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> <500BB792.9020401@jaist.ac.jp>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 7/22/2012 3:19 AM, Christian Sternagel wrote:

What you describe is all possible without using axioms (which are usually just used to initially set up a logic like HOL in Isabelle). Just use a locale that has all your "axioms" as assumptions and inside this locale you can work as if you had introduced the axioms.

> However,

you avoid the risk of anything outside the locale being effected. E.g., when adding inconsistent axioms to HOL the combination is just inconsistent (and because of this risk I would not build on any theory with "unnecessary" axioms). Defining a locale with inconsistent assumptions just means that the locale itself is useless but does not effect the whole logic.

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.

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.

What you describe is not using HOL as a meta-language to reason about another standard logic (which is a reasonable thing to do), but extending HOL itself by additional axioms (which I would consider risky).

If an expert gives me the right information, I stop thinking that way.

If you use HOL to reason about another logic, you will *define* (not axiomatize) the formulas of this logic as HOL-type and also define its semantics by HOL-functions. In that way you can talk *about* the other logic *in* HOL. just my 2 cents, chris

Regards, GB

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

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

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

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

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