*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*: Mon, 23 Jul 2012 11:45:32 +0900*In-reply-to*: <500C22E9.3070108@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> <500BB792.9020401@jaist.ac.jp> <500C22E9.3070108@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120717 Thunderbird/14.0

Dear Gottfried, On 07/23/2012 12:57 AM, Gottfried Barrow wrote:

You say, "Don't use the GOTO statement." I say, "Okay, then be my personal tutor, and give me what will take me months to learn on my own." You say, "I'm a busy person, and everyone has to largely learn this on their own." I say, "I understand that, but I'm going to use the GOTO statement until I learn a better way."

Understandable ;)

I go on at length below, but I take your advice. If you hadn't told me explicitly that locales is what I really want, then I wouldn't know today that locales is the goal I'm supposed to shoot for.

That idea has occurred to me some. The m number of HOL axioms haven't been shown to be inconsistent, and my desired 10 axioms haven't been shown to be inconsistent. I talk about FOL on top of HOL, but I know that it's really a logic 10 + m axioms, so the question becomes, "Has anyone proved that the 10 + m axioms together are inconsistent?" If you tell me the answer is yes, then I listen to you because you have good credentials. If you tell me, "I don't even know what your 10 specific axioms are", then I say, "He didn't say yes, the 10 + m axioms are inconsistent, so I'll take that as meaning no one knows".

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).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.

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?

To make a long story short, if I give Sledgehammer a theorem that's only HOL, and HOL is consistent, then Sledgehammer can only prove that the theorem is true or that its negation is false. But if I give Sledgehammer a theorem that's built on axioms, and my axioms are time tested axioms, but yet they are inconsistent, but yet not because of their combination with the HOL axioms, then Sledgehammer will try all sorts of unnatural combinations that a human would never try, with the possible result that both the theorem and its negation is proved true.

>

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.

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.So now, you talk about not merely "using a logic" but "reasoning about a logic". You should understand that a formal, mathematics education generally only gives a person the bare minimum to "use a logic". DeMorgan's laws, the equivalence (A --> B)==(~A \/ B), how to negate statements with quantifiers, proof by induction, proof by contradiction and little bit more is about all you're taught and all you need to do typical math. The math gets complicated, but the logic never does, so I think "reasoning about logic" will be m+n number of months down the road for me. But I set "reasoning about another logic" as another goal to achieve based on your advice.

cheers chris

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

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

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

- Previous by Date: Re: [isabelle] Isabelle/jedit
- Next by Date: Re: [isabelle] Isabelle/jedit
- 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