Re: [isabelle] Schematic vars or universal bound vars in theorem?
On 7/22/2012 9:45 PM, Christian Sternagel wrote:
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
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
Christian, remember, you asked. I work some to keep my speculative,
philosophical, and undereducated opinions off the list.
First, I define an acronym, FOLZFS, which means "the first-order
language of Zermelo-Fraenkel sets". Below, I use the term HOL+FOLZFS,
which would be the axioms of HOL plus my axioms, however bogus my axioms
I now pose a question to set the context for everything that's
completely driving how I'm trying to use Isabelle as a proof assistant.
QUESTION: Why am I being forced to choose between HOL and a reasonably
pure implementation of FOLZFS?
Mike Gordon was thinking about this conflict between HOL and FOLZFS a
long time ago in "Set Theory, Higher Order Logic or Both?" (PDF link
under "Download Links").
His HOLZF was the concept behind Steven Obua's src/HOL/ZF/HOLZF.thy,
written about in "Partizan Games in Isabelle HOLZF":
I continue below because our comments below are related to your question.
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
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.
The terms "meta-language" and "object-language" are fairly imprecise
terms. I'm a generalist, so I've been trying to use those terms instead
of Larry's "meta-logic" and "object-logic". I think I could justify how
I've been using them.
However, you've clarified and made clear to me two important concepts,
1) extending a logic vs. using it to define a higher-level language, and
2) reasoning about a logic vs. using a logic.
I know that I'm extending HOL, especially now, but I still want "meta".
Alright, so I try to use "meta" and conform to a reasonable dictionary
meaning. I take the definition of meta- to be "outside of".
Is HOL a usable logic? Yes. Are my FOLZFS axioms a usable logic? No. I
need HOL to implement them in a concrete way. So HOL+FOLZFS becomes the
logic, and though both HOL and FOLZFS are inside the logic, the most
important point is that HOL is outside of FOLZFS.
In fact, I say that FOL is embedded in HOL, and because my FOLZFS is
almost exclusively made of FOL formulas, where the rest is made up of
HOL functions, and where every FOL logical symbol is implemented as a
HOL function, can I not think of, for my own purposes, FOLZFS as "on top
Here, feel free to throw away what you don't want in the above paragraph.
I continue below.
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?
I'm no expert on Pure, but the many papers about Isabelle's meta-logic
emphasize primarily that Pure gives us a minimal logic of \<And>, "==>",
By default, with no HOL axioms, we have the three logical operators
above. Would it not be mathematically disciplined to build up all of the
HOL theorems from the logic available from Pure? Are there no theorems
which can be shown to be true with only those three logical operators,
and whatever it is that Pure can prove? So there are theorems that could
be proved, but those three logical operators can only get you so far
without being axiomatically extended. Here, I adopt your phrase above,
"but I might be wrong".
Makarius is basically telling me to build up my theorems only from the
available HOL axioms. It's not that I don't want to, I just don't think
I can ever get my 10 very specific FOL formulas from the m number of HOL
I tie into everything this below.
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.
Lots of tangents are getting mixed up here, but yea, part of what I'm
talking about is 100% testing. The biggest thing I got out of last week
was my script to take a theorem and run 4 different tests on it. When
testing theorems with powerful tools becomes free time-wise, it's
something I want available in my arsenal.
It's like syntax errors. It's not that you can't find them, but you can
work a whole lot faster when the IDE finds the error, takes you to the
code, and highlights the error.
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.
Now I tie back into the first three parts. If you were wrong, that's
fortunate because the two concepts I listed above are important
concepts, especially "extending a logic", where I wasn't even
considering HOL's ability to allow me to reason about another logic. It
turns out that's not what I want at all. No, I need a logic "to use". If
I can't use it, then the best I could do when reasoning about it is to
find out that I can't use it.
As to locales, compartmentalization is a good thing that I want at my
disposal as soon as possible.
I try to finish answering your question, "What exactly are you
First, there's the general concept that you take an old, existing
language, and you use it to implement another language.
For example, you take assembly language, and you create C. You take
Pure, and you create Isabelle/HOL or Isabelle/FOL.
It doesn't have to be tied into logic. We can take English, and teach
someone Chinese. We find a primitive tribe, and we use the Latin
alphabet and English morphemes to create a written language for the tribe.
There's the meta-language that we have to use, and the object-language
which we cannot create or get access to without the use of the
meta-language, at least in the formative stages.
Whether extending HOL with axioms to get FOLZFS, or coming up with a
novel solution to get the same "model" without any new axioms, HOL is
absolutely essential as the underlying language of logic (having
chosen), and I find it hard not to call HOL the meta-language for both
As to whether I'm misusing vocabulary and language, I'll let you decide,
though I might not agree with your decision.
RUNNING OUT OF STEAM
I've suddenly run out of steam to go into great detail about my
formative ideas of FOLZFS on top of HOL, so I just make a few comments.
If you want info, just ask.
HOL gives me a form of sets, but these sets cannot be used in the same
way ZF sets can be used. I make no moral judgements about that. The
application at hand is merely to explore what is achievable by either
extending HOL with axioms to get FOLZFS or find that elusive novel
solution without using axioms. The axiomatic approach is possibly more
of a no-brainer algorithm. See FOL formula in textbook? Put FOL formula
in Isabelle. Go back to "see FOL" step.
There are 9 axioms and 1 axiom scheme. I say above that "FOL is embedded
in HOL", so my assumption is that if I used 100% FOL formulas with
Isabelle/HOL, then I'm 100% safe.
Without having gone down the road very far, I replace the axiom scheme
with one axiom in which I quantify over "sT => sT => bool". One thing
leads to another. If it doesn't work, I try to figure out why, which
will require me to learn something. If I can't figure it out, I go onto
something more productive, and keep that in the back of my mind.
After reading my email over, I remembered some more reasons why I want
HOL. I had deleted the following part of your reply:
> 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.
1) Because nobody will care about my FOLZFS as a standalone logic, but
they might care about it if it's riding on the coattails of HOL.
2) I get FOL for free. Larry had to lay the groundwork for "o". I get
"bool" for free.
3) Because an exciting idea has occurred to me, an idea which is less
than 24 hours old. If I have a type, sT, that truly models ZFC sets,
then I get set classes for free with "sT set". Or do I?
ONE LAST POINT
One last point about "What exactly are you describing here?"
I'm describing an attempt to stay in HOL, or stay close to HOL because,
among other reasons, there's a larger developer base and user base, and
Isabelle/HOL is getting hundreds of thousands of dollars a year (pounds,
marks, euros) in funding.
You're one of the HOL developers, and so my question involving HOL
caught your attention. It pays to stay with HOL if you can.
This archive was generated by a fusion of
Pipermail (Mailman edition) and