*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*: Mon, 23 Jul 2012 13:05:35 -0500*In-reply-to*: <500CBACC.9000805@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> <500C22E9.3070108@gmx.com> <500CBACC.9000805@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 9:45 PM, Christian Sternagel wrote:

The scenario I just described would be completely beneficial toIsabelle/HOL as a product. What's done as HOL is just HOL, whereHOL isobviously very useful. But if HOL is used as a meta-language to implement another standard logic on top of it, in a way that'sreasonably pure, which might require axioms to do, then that'ssomethingdifferent.What exactly are you describing here? From this statement I gatheredthat you wanted to reason about your 10 axioms inside HOL (butapparently that's not the case; see below).

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7899

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.2131 I continue below because our comments below are related to your question.

What you describe is not using HOL as a meta-language to reason about another standard logic (which is a reasonable thing to do), butextending HOL itself by additional axioms (which I would considerrisky).Okay, but it seems to me there's a meta-something in there. HOL is the language that I use to implement another language, and I hide as much as possible that HOL is the primary foundation.Not exactly, you do not implement your 10 axioms *in* HOL when usingaxioms, you *extend* HOL. What I'm trying to say is that I don't seethe meta-role of HOL in your situation.

1) extending a logic vs. using it to define a higher-level language, and 2) reasoning about a logic vs. using a logic.

http://en.wikipedia.org/wiki/Meta

Here, feel free to throw away what you don't want in the above paragraph. I continue below.

Larry set up Pure so that it's the meta-logic that's used to create the object-logic HOL. HOL uses axioms. If HOL is built on Pure with axioms, then why shouldn't I add axioms to HOL to get what I want?My feeling is that Pure vs. HOL is a different story from your HOL vs.10 axioms (but I might be wrong). Pure is the logical framework ofIsabelle which just provides some infrastructure that is typicallyneeded in interactive theorem provers for many specific logics (likeunification, natural deduction, etc.). In a sense, Pure is "built-in".For a specific logic (like FOL, HOL, etc.) we give the basic axiomsonce and than work on top of them.

I tie into everything this below.

Similarly, Nitpick might prove both the theorem and its negation false. Now, because at least one of the axioms is "polluted" with a little bit of HOL, then I have to work really hard to show that the inconsistency is not because of that, but I might want that challenge.You said it yourself "the possible result". Your approach looks liketesting to me. You might find a problem, however if you don't, youhaven't learned anything new.

I was under the impression that "reasoning about the 10 axioms" iswhat you wanted to do, sorry if I was wrong. I'm not saying you shoulddo that. And you are definitely right that this would be time-consuming.cheers chris

RUNNING OUT OF STEAM

> want to achieve.

ONE LAST POINT One last point about "What exactly are you describing here?"

Regards, GB

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

**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] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] Simple question about theory parameter
- Previous by Thread: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Thread: [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