Email Gateway (Aug 18 2022 at 20:32): Email Gateway (Aug 18 2022 at 20:32):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I summarize my question first.
I have two theorems, SigmaE_is_unique and SigmaE_is_unique2. In the
first, I end up with "u" as a universally quantified bound variable,
because that's how I specified it in the formula. In the second, I end
up with "u" as a schematic variable, because I left it as a free
variable in the formula.
Which of these do I want? This question also applies to my axiom Sigma_exA.
I read this thread, "Free variables vs schematic variables":
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00048.html
I've also read this email, which is an aside:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00172.html
The context of that thread was meta-logic, so when Makarius says,
"Outermost quantifiers are circumvented... there is an explicit core
inference that removes the quantifiers and expresses the generality in
terms of schematic variables", I conclude that he's talking about the
\<And> quantifier. This is because I don't see any removal of \<forall>.
I do notice in proof steps and theorem results, that Isabelle may
rearrange a \<forall> in a formula, such as taking a \<forall> to the
outside of some parentheses. That's fine with me.
Here, I use my limited knowledge to determine the difference in my two
theorems mentioned above. If all the variables in the theorem are bound,
then the formula in the theorem will simply be used as a fact.
If there are schematic variables in the theorem, then schematic
variables will first be instantiated, and the instantiated formula of
the theorem will be used as a fact.
I don't know why I need variables to be instantiated to make it more
general, or whether I don't want variables to be instantiated so that
it's tighter.
This also applies to my axiom Sigma_exA. I can strip out all the
universal quantifiers, and everything still works, but I end up with
schematic variables being used, as shown by "thm show_info2", although
it may be the proof step of show_info2 that's really a true reflection
of Sigma_EeA, in which the variables are still free.
I attached the theory, where some names above are rough translations.
Thanks,
GB
sTs_.thy
Email Gateway (Aug 18 2022 at 20:32):From: Gottfried Barrow <gottfried.barrow@gmx.com>
This reply to my email is a basic logic fix, in case it matters to someone.
For my equality axiom, I was using something like this:
(1) "!u. !v. !x. ((x <\in> u <-> x <\in> v) --> u=v)",
with a corresponding theorem like this:
(2) "!u. !x. (~(x \<in> u) --> u = Sigma_E)".
The textbook formula came to my mind, so I changed the axiom to:
(3) "!u. !v. ((!x.(x \<in> u <-> x \<in> v)) --> u=v)".
Which then required a corresponding change to my theorem to not get an
error:
(4) "!u. ((!x. ~(x \<in> u)) --> u = Sigma_E)".
My questions about schematic vs. universal bound variables stay the same.
Regards,
GB
Email Gateway (Aug 18 2022 at 20:32):From: John Wickerson <jpw48@cam.ac.uk>
I think you should state the theorem without the \<forall>, because it makes it easier to use the theorem later on. For instance, you can say
... using SigmaE_is_unique[of "foo"]...
to obtain SigmaE_is_unique in the case when u is foo. You can't do this so easily when you have the \<forall> there.
john
Email Gateway (Aug 18 2022 at 20:33):From: Gottfried Barrow <gottfried.barrow@gmx.com>
John,
That sounds like it could be the biggest reason. I was only thinking
about schematic variables being instantiated automatically. The idea of
calling theorems like in a programming language hasn't occurred to me,
until now.
So, I guess I want a schematic variable in a theorem when I know I'm
going to want to instantiate it manually. However, I now have the
question of whether automatic proof methods need the schematic variables
so that they can instantiate them.
It's my healthy paranoia kicking in here. I'm using axioms, so I'm
trying to use everything I know right now to keep from being inconsistent.
Another question I would have for a person is whether I'm protected in
any way by making a variable bound so that it doesn't become a schematic
variable.
Thanks,
GB
Email Gateway (Aug 19 2022 at 07:48):From: Makarius <makarius@sketis.net>
The best way is not to use axioms then. In mathematics you define new
things by using old ones, and then prove the desired properties.
Sometimes you work with abstract theories, but that corresponds to a
locale or class definition in Isabelle/HOL, not axiomatization.
Makarius
Email Gateway (Aug 19 2022 at 07:49):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I'll try to make a short sales speech here to spin the pro-axiom side of
things.
Suppose there are 10 standard axioms for a language of FOL that have
held up for many years. Then there's no more risk in using those axioms
than there's ever been.
Suppose a person implements those axioms on top of Isabelle/HOL with a
slight modification, and others build a lot of standard math on top of
those axioms, and no inconsistency shows up.
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.
I'm interested in certain non-applied math, but with Isabelle I take the
attitude that all math implemented in Isabelle is applied math, with the
application being the attempt to find out how powerful Isabelle is. If
no one successfully uses axioms on top of Isabelle/HOL, then that
potential power of Isabelle/HOL never gets demonstrated.
Church's logic was shown to be inconsistent. The possibility of that
happening is all part of the game.
Giving opinions. That's the easy part.
Regards,
GB
Email Gateway (Aug 19 2022 at 07:49):From: Christian Sternagel <c-sterna@jaist.ac.jp>
What you describe is all possible without using axioms (which are
usually just used to initially set up a logic like HOL in Isabelle).
Just use a locale that has all your "axioms" as assumptions and inside
this locale you can work as if you had introduced the axioms. However,
you avoid the risk of anything outside the locale being effected. E.g.,
when adding inconsistent axioms to HOL the combination is just
inconsistent (and because of this risk I would not build on any theory
with "unnecessary" axioms). Defining a locale with inconsistent
assumptions just means that the locale itself is useless but does not
effect the whole logic.
The bottom line: avoid using axioms (as long as you are not setting up a
new object logic for Isabelle).
On 07/22/2012 03:29 PM, Gottfried Barrow wrote:
On 7/21/2012 1:32 PM, Makarius wrote:
On Wed, 18 Jul 2012, Gottfried Barrow wrote:
It's my healthy paranoia kicking in here. I'm using axioms, so I'm
trying to use everything I know right now to keep from being
inconsistent.The best way is not to use axioms then. In mathematics you define new
things by using old ones, and then prove the desired properties.
Sometimes you work with abstract theories, but that corresponds to a
locale or class definition in Isabelle/HOL, not axiomatization.I'll try to make a short sales speech here to spin the pro-axiom side of
things.Suppose there are 10 standard axioms for a language of FOL that have
held up for many years. Then there's no more risk in using those axioms
than there's ever been.
Right, but combining those axioms with others (say those of HOL) is a risk.Suppose a person implements those axioms on top of Isabelle/HOL with a
slight modification, and others build a lot of standard math on top of
those axioms, and no inconsistency shows up.
This sounds all very risky ;) "a person" (as in a single person),
"slight modification", "no inconsistency shows up".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 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).
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.
just my 2 cents,
chris
Email Gateway (Aug 19 2022 at 07:50):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 7/22/2012 3:19 AM, Christian Sternagel wrote:
What you describe is all possible without using axioms (which are
usually just used to initially set up a logic like HOL in Isabelle).
Just use a locale that has all your "axioms" as assumptions and inside
this locale you can work as if you had introduced the axioms.
Christian, I'd be more than happy to take a disciplined approached, but
how is it possible for a beginner to take a disciplined approach and
develop what normally should be developed by an advanced user? It's not.
However, I don't want anyone to consider me as complaining about
Isabelle, because I've ceased to have any complaints about it. There are
no problems with Isabelle. There are only workarounds, and I can't think
of any significant workaround that I'm having to resort to yet.
I'm also more than happy to be told two things by experts: that a
certain thing has been proved to be wrong or impossible, or that a
particular way is the right way to do something.
You tell me locales is what I want, and I listen to you, and I make it
my goal to learn how to use locales in place of axioms. But I search on
"locale" in prog-prove.pdf and in tutorial.pdf and it doesn't show up. I
open up locales.pdf, which is 20 pages long, and I briefly look at it. I
conclude, locales is m number of months down the road.
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."
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.
However,
you avoid the risk of anything outside the locale being effected. E.g.,
when adding inconsistent axioms to HOL the combination is just
inconsistent (and because of this risk I would not build on any theory
with "unnecessary" axioms). Defining a locale with inconsistent
assumptions just means that the locale itself is useless but does not
effect the whole logic.
Now we're in the territory that what's important to two different people
doesn't necessarily intersect.
You care that your theories don't make Isabelle/HOL inconsistent, and I
want you to care about that because I would hate for you to give me a
HOL product that would allow me to prove everything.
Today, right now, I only care about a particular language of FOL that I
want to "put on top" of HOL with some minimal number of HOL functions
that are required to make it practical.
If I introduce inconsistency (not because of combining HOL axioms with
mine), what difference does it make if I mess up a locale or all of
Isabelle/HOL? I'm not bummed that I messed up HOL. I'm bummed that my
axioms didn't work out.
In fact, it's possible that the best way for me to look for flawed logic
fast is to use axioms, where "fast" is a synonym for Sledgehammer and
Nitpick. I wait to say more about that below.
Suppose there are 10 standard axioms for a language of FOL that have
held up for many years. Then there's no more risk in using those axioms
than there's ever been.
Right, but combining those axioms with others (say those of HOL) is a risk.
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".
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 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. If nobody imports my theory
with the additional axioms, then the standard Isabelle/HOL distribution
is completely unchanged.
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?
Well, I shouldn't; that's what we're discussing. But now we're back into
end goals and purpose. For your purposes, no axiom should ever be added
to HOL. For my purposes, there is a seed that's been planted which gives
me the thought that I may want axioms in spite of being able to use
locales for the same purpose.
If an expert gives me the right information, I stop thinking that way.
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.
I've already learned things that I wouldn't have learned if I wouldn't
have been using axioms.
Here, I point out that anything I've said above could be totally flawed.
However, good things can come out of clueless people using software in
unorthodox ways that initially appall the developers.
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.just my 2 cents,
chris
And so your 2 cents is very valuable due to the exchange rate between my
economy of the beginner and your economy of the expert.
Let's say that due to the weakness of my beginner's economy, 2 cents in
your economy of the expert is worth at least $150 in my economy. I make
that estimate because I figure you could charge $150 an hour working in
U.S. industry as a consultant, maybe more or maybe less, not that a
price can really be put on the value of information provided by an
expert, because it generally takes a person years to obtain expert
knowledge.
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.
Regards,
GB
Email Gateway (Aug 19 2022 at 07:50):From: Gottfried Barrow <gottfried.barrow@gmx.com>
I read my emails over and over again before I send them out, but I still
end up having to clutter up the list with two emails instead of one to
clarify something.
Sledgehammer proves things true. Nitpick proves things false. Like I
said, negative logic can mess me up in the most simple ways.
Explicitly correcting what I said, if a logic is consistent, then
Sledgehammer can prove a theorem true or proves its negation true, but
not both.
Regards,
GB
Email Gateway (Aug 19 2022 at 07:50):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 19 2022 at 07:50):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
Larry Paulson
Email Gateway (Aug 19 2022 at 07:51):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 07:51):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
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).
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").
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.7899
His HOLZF was the concept behind Steven Obua's src/HOL/ZF/HOLZF.thy,
written about in "Partizan Games in Isabelle HOLZF":
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.2131
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".
http://en.wikipedia.org/wiki/Meta
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.cheers
chris
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.
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
[message truncated]
Last updated: Nov 21 2024 at 12:39 UTC