Email Gateway (Aug 19 2022 at 09:26): Email Gateway (Aug 19 2022 at 09:26):From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,
Thank you all for helping me with the considerable amount of questions I
posted in the list
throughout this year. After some reluctance
over the last couple of years I have finally decided to tackle my
experiments in Isabelle a bit more
seriously.
Anyway, I finish this e-mail by posting the link from a post by Andrej
Bauer on the role
of free and bound variables. This topic seems to be the one which was
amongst the
topics most discussed in the list during this year.
"Free variables are not "implicitly universally quantified"!
http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/
All the Best!
Email Gateway (Aug 19 2022 at 09:36):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Alfio,
So last year I went over my allotted quota for talking about free
variables and whether they're really implicitly quantified in Isabelle.
However, this is now the year 2013.
(Here, after writing everything below, it has occurred to me that I
might have taken all this way too serious, but as I say below, I have
some time on my hands.)
Really, many arguments just reflect the limitations of natural language,
that because communication with natural language tends to be a single
pipelined activity, the complete context influencing one human mind is
not transmitted very well to another human mind, and we all know, or
should know, that context is everything.
With "free variables are not implicitly universally quantified", I could
go on lots of tangents, but I'll limit myself to two, and a conclusion
or two.
One is that sometimes, if I'm given a precise, definitive, useful answer
on a subject I've been arguing about, I lose interest in the argument
because I become much more interested in the answer, which sometimes is
simply because the answer is so definitive, there's nothing to argue
about anymore, and what I could find to argue about is no longer that
interesting in light of the new answer.
(Not having slipped this in anywhere else in the past, I got a
definitive, precise answer on the HOL4 list from Josef Urban by means of
this wiki article and his short example of how to use the algorithm
given in the article:
https://en.wikipedia.org/wiki/Extension_by_definitions
Why would I want to have continued to argue about what I was arguing
about after I was given an algorithm I could use? Getting the algorithm
was a major discovery. That I didn't learn about it from those other
group of people is a bad mark against them. Other senior members on that
list also helped me out too, but that wiki article and how to use it
will potentially be very important in the future for me.)
Another tangent is that there is abstract language, language used to
"get theoretical" as they say, and there is language which is
extraordinarily precise and concrete, such as ML and the machine
language it is ultimately reduced to.
So Andrej Bauer is at a major disadvantage in discussing whether free
variables are implicitly universally quantified, because in his
discussion, the phrase "free variables are implicitly universally
quantified" is important, even if it is used informally to get to a
formal end of things.
With a proof assistant such as Isabelle, the phrase "free variables are
implicitly universally quantified" is an attempt to describe what the
software is doing, but ultimately, the meaning of the phrase has no
bearing on what the software does once the developer hits the compile
button. To describe some things that the Isabelle code does, "free
variables are implicitly universally quantified" is probably the best
phrase to use, but if the phrase isn't used, it changes nothing. The
code is compiled in stone, until it's compiled again. Decisions have
been made to make concrete what has been theoretical and abstract.
With my limited knowledge, I take a shot at critiquing Andrej's post.
I think his reasoning for "Reason 6" could be a little faulty, that is, his
Perhaps we can just forbid free variables altogether and stipulate
that all variables must always
be quantified. But how are you then going to prove (\forall x \in
R. phi). The usual way
'Consider any x \in R. Then bla bla bla, therefore phi.'
is now forbidden because the first sentence introduces x as a free
variable.
But the statement (\forall x \in R) as a standalone statement doesn't
even make sense, so x couldn't be used as anything other than a free
variable and have it make sense, in the traditional context of free and
bound variables.
How about if we say, "All variables must be quantified except for
variables in atomic formulas"? Kind of like how you start out in
first-order logic. If x and y are variables, and if f is an binary
relation, then f(x,y) is a formula. It wouldn't make any sense to be
quantifying the variables in an atomic formula.
So, possibly, there wouldn't a problem with all variables being
implicitly quantified, except for variables in atomic formulas, at least
to deal with his simple example.
Okay, here I can ask the question, "In Isabelle, are all free variables
implicitly universally quantified?".
To tie back into Andrej's example, in Isabelle, in certain contexts, it
appears that free variables are implicitly universally quantified, but
yet in Isabelle, there's an equivalent to Andrej's "Consider any (x \in
R)", so it appears in Isabelle, there's no conflict between free
variables being implicitly universally quantified and having free
variables available to say "Let x be a real number."
But I wouldn't know. I haven't seen that in Isabelle it's been
established that "all free variables are implicitly universally
quantified". Some implications were shown, but exactly what's happening
at the meta-logic level wasn't shown in detail.
But I would say that Andrej's discussion is a different discussion than
any discussion about free variables in Isabelle. Take his "Consider any
x \in R". What is its exact meaning? It doesn't have an exact meaning.
On the other hand, Isabelle's equivalent of saying "Let x be a real
number" has an exact meaning, along with the rules in which "free
variables get implicitly universally quantified", under whatever
contexts those rules hold. The point is that the game changes when the
abstract has been made precise and concrete.
Anyway, I put his blog in my RSS reader, and I'm backing up about 240
Gbytes of data to 8 Gbyte DVDs, so I have some time on my hands.
Regards,
GB
Email Gateway (Aug 19 2022 at 09:37):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Alfio,
On 01/02/2013 01:54 PM, Gottfried Barrow wrote:
On 12/30/2012 7:50 AM, Alfio Martini wrote:
Anyway, I finish this e-mail by posting the link from a post by Andrej
Bauer on the role
of free and bound variables. This topic seems to be the one which was
amongst the
topics most discussed in the list during this year."Free variables are not "implicitly universally quantified"!
http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/
just a remark: I think what Andrej Bauer is writing about is different
from what is usually discussed on the Isabelle mailing lists. I don't
think that anybody ever thought or claimed that Isabelle logically
equates a formula with its universal closure. The discussions are
usually about: what is the exact meaning if I write something like
lemma "P x"
where "P" is some formula with the free variable "x". In this context, a
helpful answer is that free variables are implicitly universally
quantified. A more cautious answer would be something like:
When writing a top-level lemma statement like 'lemma "P x"' Isabelle
behaves as if the free variable "x" was universally quantified at the
meta-level for almost all purposes ;)
dear Gottfried,
(Not having slipped this in anywhere else in the past, I got a
definitive, precise answer on the HOL4 list from Josef Urban by means of
this wiki article and his short example of how to use the algorithm
given in the article:https://en.wikipedia.org/wiki/Extension_by_definitions
An answer to what question? What algorithm do you mean? And how do you
relate this article to the topic of "free/bound variables"?
That I didn't learn about it from those other
group of people is a bad mark against them.
What is that supposed to mean?
happy new year,
chris
Email Gateway (Aug 19 2022 at 09:38):From: Alfio Martini <alfio.martini@acm.org>
Dear Christian,
just a remark: I think what Andrej Bauer is writing about is different from
what is usually discussed on the Isabelle mailing lists. I don't think that
anybody ever thought or claimed that Isabelle logically equates a formula
with its universal closure
You are right. In the way I put it, the relationship between Andrej´s
article and the actual discussion carried in
the list sounds (quite?) a bit misleading.
However, it was a kind of provocative attempt to bring the topic again. The
answers were all there, spread through
a number of different posts (and flames). Maybe I secretly wanted to begin
this new year with a nice summary
of that discussion.
what is the exact meaning if I write something like
lemma "P x"
where "P" is some formula with the free variable "x". In this context, a
helpful answer is that free variables are implicitly universally
quantified. A more cautious answer would be something like:
When writing a top-level lemma statement like 'lemma "P x"' Isabelle
behaves as if the free variable "x" was universally quantified at the
meta-level for almost all purposes ;)
One could hardly have done better than that.
In fact, in my humble opinion, a more appropriate title for Andrej´s
article would be along the lines of
"When free variables can be considered as universally quantified?" or even
"On the role of [free, bound and quantified] variables in Computing and
Mathematics"
So, it depends on the context, as you rightly put it above. In the same
way, here in the list, everything we were discussing
in these several [related] threads was essentially tied to the question
"When free variables are treated [interpreted] as universally quantified
[in Isabelle]?"
Now I can finally move on.
All the Best!
On Fri, Jan 4, 2013 at 2:43 AM, Christian Sternagel <c-sterna@jaist.ac.jp>wrote:
Dear Alfio,
On 01/02/2013 01:54 PM, Gottfried Barrow wrote:
On 12/30/2012 7:50 AM, Alfio Martini wrote:
Anyway, I finish this e-mail by posting the link from a post by Andrej
Bauer on the role
of free and bound variables. This topic seems to be the one which was
amongst the
topics most discussed in the list during this year."Free variables are not "implicitly universally quantified"!
http://math.andrej.com/2012/**12/25/free-variables-are-not-**
implicitly-universally-**quantified/<http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/>just a remark: I think what Andrej Bauer is writing about is different
from what is usually discussed on the Isabelle mailing lists. I don't think
that anybody ever thought or claimed that Isabelle logically equates a
formula with its universal closure. The discussions are usually about: what
is the exact meaning if I write something likelemma "P x"
where "P" is some formula with the free variable "x". In this context, a
helpful answer is that free variables are implicitly universally
quantified. A more cautious answer would be something like:When writing a top-level lemma statement like 'lemma "P x"' Isabelle
behaves as if the free variable "x" was universally quantified at the
meta-level for almost all purposes ;)dear Gottfried,
(Not having slipped this in anywhere else in the past, I got a
definitive, precise answer on the HOL4 list from Josef Urban by means of
this wiki article and his short example of how to use the algorithm
given in the article:An answer to what question? What algorithm do you mean? And how do you
relate this article to the topic of "free/bound variables"?That I didn't learn about it from those other
group of people is a bad mark against them.
What is that supposed to mean?
happy new year,
chris
Email Gateway (Aug 19 2022 at 09:43):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 1/3/2013 10:43 PM, Christian Sternagel wrote:
(Not having slipped this in anywhere else in the past, I got a
definitive, precise answer on the HOL4 list from Josef Urban by means of
this wiki article and his short example of how to use the algorithm
given in the article:https://en.wikipedia.org/wiki/Extension_by_definitions
An answer to what question? What algorithm do you mean? And how do you
relate this article to the topic of "free/bound variables"?
Christian,
If I wouldn't have wrote the last email, that wouldn't have been a bad
thing.
Anything I say more can be interpreted overall as me saying, "Hey,
thanks all you developers for a great product. It's like the World Wide
Web and the Internet, and technology in general. The newness can wear
off, but I sometimes I still get that feeling again of 'this is awesome'".
HOW DO I RELATE IT TO...? (PART 1)
The article, as part of an answer by Josef, is related to my tangent in
my last email. There is "trying to prove your point logically", and then
there are "facts". Facts, once I'm aware of them, can change a whole lot
of things, motivation being one of them.
You and Josef gave me facts. Prior to your example showing conclusively
that implicit quantification is happening in Isabelle for free
variables, Andrej's blog post might have put me in the "Hmmm, this has
me worried. I need to think about this a whole lot to understand all of
this."
But now, knowing the fact that implicit quantification is happening in
Isabelle, I say, "Well, Andrej, you say it's bad for people to say 'a
free variable is implicitly universally quantified', but with Isabelle,
they don't just say it, they go a step further and, for all practical
purposes, hardwire that concept in the code, at least for the logic that
would apply to the examples in your post, which would be first-order
logic. As to there being any problems and limitations with doing that, I
don't know what those would be. Others can fight those battles if there
are battles that need to be fought."
In the last email, I said his discussion is a different discussion, but
surely it's still related. In his "Reason 6", he's making a big deal
about us needing to be able to do a "Universal Generalization" proof,
that is, by starting out with a arbitrary but fixed element of the real
numbers, which, according to him, must be free, as represented by his
"Consider any x /in R".
(Here, I may sound like I know that I know what I'm talking about, but
what I actually know is that I occasionally make a good point, but,
otherwise, am very wrong much of the time. I also attached a pertinent
image from Bloch's "Proofs and Fundamentals". I love even basic books
like that, but I wish my formal education would have started me out at a
lower level, so I wouldn't have wasted so much time on discovery.)
So the facts you and Josef have given me have changed the nature of
certain debates.
That Andrej is making a valid point, I assume he is. That I can learn
something from him, well, I have learned something from his Epilogue,
which basically tells me what Bloch's book tells me, that Universal
Instantiation is equivalent to Universal Generalization, but by him
saying it, it drives home a point that otherwise wouldn't have gotten
driven home, especially because of our recent Isabelle "implicit
quantification" discussion.
But back to facts and their value.
Adrej is getting dogmatic, which might have made me want to get dogmatic
with him, but now I know certain facts, and I say, "Andrej, your
discussion is ill-defined anyway. The Isabelle proof assistant has exact
meaning in every statement we can make, and it could be that Isabelle's
'Consider any x \in R' just becomes part of a big conjunction, which
means we aren't truly doing a Universal Generalization proof. If we
can't, then we can't. I'm not worried about it. Whatever the case, with
Isabelle, there's something there rock solid to crtitique and attack if
there's a problem."
The last sentence was part of my "Hey, developers. Is Isabelle a great
product, or what?" That the complement might come at some other people's
expense, that can happen, and I touch on that below.
HOW DO I RELATE IT TO...? (PART 2)
Mentioning the wiki article was a way to say something good about the
people that contribute to the HOL4 mailing list, rather than to wait for
some unlikely future date in which my complement would be completely on
topic.
AN ANSWER TO WHAT QUESTION?
Here, if I didn't give you this link, that wouldn't be a bad thing, but
there is some good information in the thread, in particular, the
culmination of it all for me in which Josef gives me the Wiki link, and
enough of an explanation that I was able to figure out the rest on my own.
The eventual, precise question was, "Can you give me a first-order
formula which uses no constants for the formula 'the empty set is in the
empty set'".
The very precise answer was given by Josef here:
WHAT ALGORITHM DO YOU MEAN?
The algorithm that Josef demonstrates when he converts "0 \in 0" to a
FOL formula which only uses variables.
That I didn't learn about it from those other
group of people is a bad mark against them.
What is that supposed to mean?
And if I didn't explain the meaning of that statement, it wouldn't be a
bad thing. After all, to bash this other group of people on this mailing
list is in bad taste.
However, this other group of people is the group of people from which I
got my formal education and looked to for answers after getting my
degree, where my formal education is a B. S. in math. "Group" would mean
mathematicians as a whole. I don't actually have any substantial
complaints about those mathematicians who were my professors.
My particular comment is related to the fact that in set theory books,
I've repeatedly read that "in principle" we could do all set theory
using first-order formulas, but we don't because it's way too
impractical to actually do any of that, even just a little.
I accepted that at face value, until I learned just enough first-order
logic to start getting serious about learning axiomatic set theory. At
that point, I started to challenge their "in principle" statement
because I started to see that first-order logic needs to immediately be
supplemented as a language to be used.
I thought that there had to be symbols in the first-order logic
specification to allow us to define constant symbols. Josef showed me I
was wrong.
Why didn't I learn that from that other group of people? At the bedrock
of ZF sets is the requirement that zero constants are given to us.
That's not little. That's huge. The FOL specification allows constants
to be given in a FOL language, but none are given to us, and
immediately, after the first ZF axiom, set theorists start introducing
constants. Now, after knowing what I'm looking for, I can see that a few
mention it, but what's in the Wiki article doesn't appear to be the
common knowledge that it should be.
I stop here, but I have a certain amount of cynicism about that other
group. I can find ways to thank them later, but what have they done to
help me be independent and get proof review? Nothing.
Regards,
GB
Universal instantiation and generalization.jpg
Email Gateway (Aug 19 2022 at 09:48):From: Makarius <makarius@sketis.net>
This thread is again in danger of getting long, so here are just some
quick jokes from the Isabelle repertoire:
* Free variables are "fixed" (in a local context).
This terminology is stemming from Mizar and used in Isar as well, but
is actually an oxymoron. Such variables are not variable at all.
* Schematic variables are "arbitrary" (after having left the context).
This is a useful formal device to make the variability of variables
formally clear.
So a properly fixed local variable acts like a local context that becomes
arbitrary after leaving it. In Isar this reads like this:
{
fix x :: 'a
have "B x" sorry
}
note B a
note B b
note B c
In fact we can make this arbitrariness stronger within the logical
framework:
{
fix x :: 'a
have "B x" sorry
}
note ⋀x. B x
Here it now looks as if the system would insert that postulated implicit
quantifier, but it is actually not there, and bypassed in the internal
reasoning. These are just two ways to specify the same result: inspecting
the machine state in the Output window, you will see schematic variables,
not quantifiers.
Next joke: What about a free variable that is not properly "fixed"?
Answer: it is an illegal immigrant into the logical context, without legal
papers. Practically it acts like an unspecified global constant, and can
usually not be used productively in a proof.
This is the reason why Isar merely prints undeclared free variables with
certain markup, but does not reject them: they are useful in
pseudo-proofs, i.e. proof patterns like above. The variables B, a, b, c
are all been illegal immigrants, without anybody getting confused.
Here is one of the rare proofs where a totally undeclared formal entity
can be used in a productively:
theorem Drinker's_Principle: "∃x. drunk x ⟶ (∀x. drunk x)"
proof cases
assume "∀x. drunk x"
then have "drunk alien ⟶ (∀x. drunk x)" ..
then show ?thesis ..
next
assume "¬ (∀x. drunk x)"
then obtain a where a: "¬ drunk a" by blast
have "drunk a ⟶ (∀x. drunk x)"
proof
assume "drunk a"
with a show "∀x. drunk x" by contradiction
qed
then show ?thesis ..
qed
The alien does not need formal declaration at the custom's office, but I
usually prefer to put a 'fix' in the proper spot nonetheless.
Makarius
Email Gateway (Aug 19 2022 at 09:49):From: Makarius <makarius@sketis.net>
I am not yet fully satisfied.
My preferred example is:
lemma "x = x"
When you write that in a context with undeclared x and (and its implicitly
inferred most general type 'a with undeclared 'a), the system will
implicitly augment the proof context by fix x :: 'a (and fix type 'a
beforehand as well).
['a::TYPE, x::'a] is the so-called "Eigen-context" of the statement.
There are two sides of this valuable coin:
(1) The proof context has its elements are fixed.
(2) The result (after export from the context) has makes them arbitrary.
The example above includes the situation for types as well, since it hints
at the important principle of implicit polymorphism in the manner of
Hindley-Milner. The type language does not even have quantifiers, so
there is no danger of claiming that they are introduced and eliminated
somewhere in the belly of the logic -- they are simply not there.
Nonetheless, there is a slight difference in free term variables and free
type variables: terms need to be fixed explicitly if meant to be universal
in the end, but types are fixed implicitly according to the possibilities
of the syntactic context.
Instead, when you write
lemma "!!x :: 'a. x = x"
you will have to fix the element in the proof before getting to the same
proof context as before:
proof -
fix x :: 'a
...
qed
This is called "formal noise" in Isar terminology. Here is the well-known
explicit way to avoid it:
lemma
fixes x :: 'a
shows "x = x"
proof -
...
qed
So you build up a context with fixed x, then you state "x = x", in the end
you get arbitrary "?x::?'a = ?x".
Makarius
Email Gateway (Aug 19 2022 at 09:52):From: Christian Sternagel <c.sternagel@gmail.com>
On 01/08/2013 01:23 AM, Makarius wrote:
On Fri, 4 Jan 2013, Christian Sternagel wrote:
lemma "P x"
where "P" is some formula with the free variable "x". In this context,
a helpful answer is that free variables are implicitly universally
quantified. A more cautious answer would be something like:When writing a top-level lemma statement like 'lemma "P x"' Isabelle
behaves as if the free variable "x" was universally quantified at the
meta-level for almost all purposes ;)
Sorry for the confusion. What I really meant was that after a successful
proof
lemma "P x"
and
lemma "!!x. P x"
behave alike (for almost all purposes). I did not even consider what
happens inside the corresponding proof. Your explanations are
enlightening (though, maybe not the uninitiated ;)).
cheers
chris
I am not yet fully satisfied.
My preferred example is:
lemma "x = x"
When you write that in a context with undeclared x and (and its
implicitly inferred most general type 'a with undeclared 'a), the system
will implicitly augment the proof context by fix x :: 'a (and fix type
'a beforehand as well).['a::TYPE, x::'a] is the so-called "Eigen-context" of the statement.
There are two sides of this valuable coin:(1) The proof context has its elements are fixed.
(2) The result (after export from the context) has makes them arbitrary.
The example above includes the situation for types as well, since it
hints at the important principle of implicit polymorphism in the manner
of Hindley-Milner. The type language does not even have quantifiers, so
there is no danger of claiming that they are introduced and eliminated
somewhere in the belly of the logic -- they are simply not there.Nonetheless, there is a slight difference in free term variables and
free type variables: terms need to be fixed explicitly if meant to be
universal in the end, but types are fixed implicitly according to the
possibilities of the syntactic context.Instead, when you write
lemma "!!x :: 'a. x = x"
you will have to fix the element in the proof before getting to the same
proof context as before:proof -
fix x :: 'a
...
qedThis is called "formal noise" in Isar terminology. Here is the well-known
explicit way to avoid it:lemma
fixes x :: 'a
shows "x = x"
proof -
...
qedSo you build up a context with fixed x, then you state "x = x", in the
end you get arbitrary "?x::?'a = ?x".Makarius
Last updated: Nov 21 2024 at 12:39 UTC