Re: [isabelle] Schematic vars or universal bound vars in theorem?
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."
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
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.
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.
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".
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).
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
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.
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.
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.
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?
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 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.
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.
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 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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and