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



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





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