*To*: Christian Sternagel <c-sterna at jaist.ac.jp>, Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Schematic vars or universal bound vars in theorem?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 23 Jul 2012 09:03:37 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*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>

Personally, I think there is nothing wrong with asserting some axioms as the foundation of a brand-new development. If they are inconsistent, your work is worthless, but if they are the sole basis of your work, putting them in a locale wouldn't change things even a little bit. If you already have a sound and working development, that's a different situation altogether. Then it would make sense to encapsulate the axioms. Larry Paulson On 23 Jul 2012, at 03:45, Christian Sternagel wrote: > 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. > Maybe I should put my claim into perspective: I *think* locales are the way to go for you. However, I do not even know what exactly you are heading at. > >> 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". > I don't even know what your 10 specific axioms are. That does not mean that no one knows, only that I don't know. > >>>> 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 exactly are you describing here? From this statement I gathered that you wanted to reason about your 10 axioms inside HOL (but apparently that's not the case; see below). > >>> 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. > Not exactly, you do not implement your 10 axioms *in* HOL when using axioms, you *extend* HOL. What I'm trying to say is that I don't see the meta-role of HOL in your situation. > >> 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 of Isabelle which just provides some infrastructure that is typically needed in interactive theorem provers for many specific logics (like unification, natural deduction, etc.). In a sense, Pure is "built-in". For a specific logic (like FOL, HOL, etc.) we give the basic axioms once and than work on top of them. > > When you extend HOL by + 10 axioms I don't see why you could just use your 10 axioms as the basis for a different logic (but again, I don't even know your specific axioms). Maybe it would help if you could describe precisely (and preferably compactly) what it is that you want to achieve. > >> 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. > You said it yourself "the possible result". Your approach looks like testing to me. You might find a problem, however if you don't, you haven't learned anything new. > >>> 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. > I was under the impression that "reasoning about the 10 axioms" is what you wanted to do, sorry if I was wrong. I'm not saying you should do that. And you are definitely right that this would be time-consuming. > > cheers > > 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

**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] [Q]Question about Isabelle/hol
- Next by Date: [isabelle] HOLCF's continuity with partially defined operators
- 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