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

On 7/22/2012 9:45 PM, Christian Sternagel wrote:
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 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).

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

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.

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.

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, which are:

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 of" HOL?

Here, feel free to throw away what you don't want in the above paragraph.

I continue below.

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.

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>, "==>", 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 axioms.

I tie into everything this below.

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.

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 describing here?"

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

As to whether I'm misusing vocabulary and language, I'll let you decide, though I might not agree with your decision.


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