# 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
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/

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

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