*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] Happy New Year with Free/Bound Variables*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Fri, 4 Jan 2013 06:32:14 -0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50E65E01.8090909@jaist.ac.jp>*References*: <CAAPnxw0gWXKFY0KdkZoy0kBHe-PY4_om6a_0GjCqecJaO-ZUGA@mail.gmail.com> <50E3BD98.7080706@gmx.com> <50E65E01.8090909@jaist.ac.jp>*Sender*: alfio.martini at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Happy New Year with Free/Bound Variables***From:*Makarius

**References**:**Re: [isabelle] Happy New Year with Free/Bound Variables***From:*Gottfried Barrow

**Re: [isabelle] Happy New Year with Free/Bound Variables***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Happy New Year with Free/Bound Variables
- Next by Date: [isabelle] New AFP entry: Computing Square Roots using the Babylonian Method
- Previous by Thread: Re: [isabelle] Happy New Year with Free/Bound Variables
- Next by Thread: Re: [isabelle] Happy New Year with Free/Bound Variables
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list