Re: [isabelle] Happy New Year with Free/Bound Variables

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"!

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:

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.


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