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
This archive was generated by a fusion of
Pipermail (Mailman edition) and