Re: [isabelle] Happy New Year with Free/Bound Variables
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Happy New Year with Free/Bound Variables
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Tue, 01 Jan 2013 22:54:48 -0600
- In-reply-to: <CAAPnxw0gWXKFY0KdkZoy0kBHe-PY4_om6a_0GjCqecJaO-ZUGA@mail.gmail.com>
- References: <CAAPnxw0gWXKFY0KdkZoy0kBHe-PY4_om6a_0GjCqecJaO-ZUGA@mail.gmail.com>
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
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
topics most discussed in the list during this year.
"Free variables are not "implicitly universally quantified"!
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
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:
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and