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