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



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





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