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

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.

Christian, I'd be more than happy to take a disciplined approached, but how is it possible for a beginner to take a disciplined approach and develop what normally should be developed by an advanced user? It's not.

However, I don't want anyone to consider me as complaining about Isabelle, because I've ceased to have any complaints about it. There are no problems with Isabelle. There are only workarounds, and I can't think of any significant workaround that I'm having to resort to yet.

I'm also more than happy to be told two things by experts: that a certain thing has been proved to be wrong or impossible, or that a particular way is the right way to do something.

You tell me locales is what I want, and I listen to you, and I make it my goal to learn how to use locales in place of axioms. But I search on "locale" in prog-prove.pdf and in tutorial.pdf and it doesn't show up. I open up locales.pdf, which is 20 pages long, and I briefly look at it. I conclude, locales is m number of months down the road.

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

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.

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

Now we're in the territory that what's important to two different people doesn't necessarily intersect.

You care that your theories don't make Isabelle/HOL inconsistent, and I want you to care about that because I would hate for you to give me a HOL product that would allow me to prove everything.

Today, right now, I only care about a particular language of FOL that I want to "put on top" of HOL with some minimal number of HOL functions that are required to make it practical.

If I introduce inconsistency (not because of combining HOL axioms with mine), what difference does it make if I mess up a locale or all of Isabelle/HOL? I'm not bummed that I messed up HOL. I'm bummed that my axioms didn't work out.

In fact, it's possible that the best way for me to look for flawed logic fast is to use axioms, where "fast" is a synonym for Sledgehammer and Nitpick. I wait to say more about that below.

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.

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

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. If nobody imports my theory with the additional axioms, then the standard Isabelle/HOL distribution is completely unchanged.

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?

Well, I shouldn't; that's what we're discussing. But now we're back into end goals and purpose. For your purposes, no axiom should ever be added to HOL. For my purposes, there is a seed that's been planted which gives me the thought that I may want axioms in spite of being able to use locales for the same purpose.

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

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.

I've already learned things that I wouldn't have learned if I wouldn't have been using axioms.

Here, I point out that anything I've said above could be totally flawed. However, good things can come out of clueless people using software in unorthodox ways that initially appall the developers.

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,


And so your 2 cents is very valuable due to the exchange rate between my economy of the beginner and your economy of the expert.

Let's say that due to the weakness of my beginner's economy, 2 cents in your economy of the expert is worth at least $150 in my economy. I make that estimate because I figure you could charge $150 an hour working in U.S. industry as a consultant, maybe more or maybe less, not that a price can really be put on the value of information provided by an expert, because it generally takes a person years to obtain expert knowledge.

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.