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



>
> 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 at 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 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<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
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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