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



On 7/23/2012 3:03 AM, Lawrence Paulson wrote:
Personally, I think there is nothing wrong with asserting some axioms as the foundation of a brand-new development. If they are inconsistent, your work is worthless, but if they are the sole basis of your work, putting them in a locale wouldn't change things even a little bit.

If you already have a sound and working development, that's a different situation altogether. Then it would make sense to encapsulate the axioms.

It helps to know that you don't think it's total loser idea, and "sole basis" would capture what I care about at this point in time. Hypothetically, in the future I'll want to be messing around with concrete numbers, so I certainly wouldn't want to be using a theory with an axiom which might mess up HOL's binary and decimal number systems.

I try to keep confessions and overflowing praise to a minimum on the list, but other theorem provers don't even allow axioms to be a point of contention, because it's set in stone what axioms we can used. Your Pure setup captures the reality of the freedom that logic gives us, which is our ability to start with any set of axioms and undefined terms we want, and see where they lead us.

Also, I've known about Isabelle/ZF and Steven Obua's HOLZF.thy, so I haven't felt completely free to talk about what it is I'm trying to do (where doing it is, of course, the hard part; concepts only get me so far).

I did look at Isabelle/ZF some. I didn't understand anything but the buzz words, but it is where I got the idea that I need 2 and only 2 types, which are your "i" and "o". It seems like that should be obvious, but if I didn't get the idea until I looked at Isabelle/ZF, it must not be accurate to describe it as an obvious idea.

I just now opened Obua's HOLZF.thy, but I closed it real quick. I know enough now to recognize a little of what he's doing, and I don't want to see his way right now. I did see axiomatization in it. After about 9 months, due to this discussion about axioms, I now have an answer as to why HOLZF is not allowed to be a part of what's imported with "imports Main".

Regards,
GB







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