*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 12 Sep 2012 14:47:18 +0100*Cc*: Gottfried Barrow <gottfried.barrow at gmx.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAPnxw2aQn-kPGodw+Bpfm5AfeeEz7PYPmtws=guNbJ=a2QsYw@mail.gmail.com>*References*: <504F99E9.8060608@gmx.com> <CAAPnxw2aQn-kPGodw+Bpfm5AfeeEz7PYPmtws=guNbJ=a2QsYw@mail.gmail.com>

Your question is about logic, not Isabelle. The formula (?x + ?y) + ?z = ?x + (?y + ?z) expresses a property about three quantities denoted by ?x, ?y and ?z. It is a convention in logic that any theorem involving free variables denotes the "universal closure" of that formula, here "all x. all y. all y. (x+y)+z = x + (y+z)". Isabelle is designed to work best a minimum of logical symbols, hence the preference for stating theorems like P1 ==> … Pn ==> Q. Hardly any mathematics paper states such theorems as !x1 … xm. P1 & … & Pn —> Q. Larry Paulson On 11 Sep 2012, at 23:26, Alfio Martini <alfio.martini at acm.org> wrote: > Dear Isabelle users > > >> Like two months ago, I specifically asked, in a fairly precise way, > "What's the >difference between free variables and universally quantified > variables, and is >there a reason I shouldn't use free variables?" > > Whenever I see this kind of discussion I remember that I am actually > interested in the (logical ) difference [in Isabelle] > between unknown variables and universally quantified variables, > > For instance, the different roles of variables in the following two > propositions : > > all x. all y. all y. (x+y)+z = x + (y+z) > > and > > (?x + ?y) + ?z = ?x + (?y + ?z). > >> From what I read, the operational meaning of the second matches the > semantics of the first. But from a logical point of view, in the second > proposition the variables are free, while in the first they are bound, > so I get confused about it. I believe I "understand" this, but then reality > strikes and I think "who am I kidding"? > > Cheers > > On Tue, Sep 11, 2012 at 5:07 PM, Gottfried Barrow > <gottfried.barrow at gmx.com>wrote: > >> Hello, >> >> It's not like I call up Bill Gates to learn about Windows 7, and if it >> sounds like I'm complaining, that would be a sound similar to complaining. >> I'm not complaining. I'm just talking because I'm allowed to. >> >> Like two months ago, I specifically asked, in a fairly precise way, >> "What's the difference between free variables and universally quantified >> variables, and is there a reason I shouldn't use free variables?" >> >> I will now give you a reasonably close, informal, one sentence answer. >> >> ANSWER: A universally quantified bound variable is a logical statement, >> where a free variable is an argument to a function. >> >> That's kind of huge difference don't you think? But two months ago, based >> on the zero answers like the above, I eventually started treating free >> variables like universally quantified variables. >> >> Who straightened me out? Nitpick. >> >> So I looked at the tutorials again, and "instantiation of free variables" >> became more clear. However, if I didn't write the software, how was I >> supposed to know how the proof engine is instantiating free variables when >> proving a theorem? Who's to say that it's not instantiating them in way >> that makes them equivalent to a universally quantified variable? Obviously >> not. >> >> This substantiates my general guiding principle that it's a fool who picks >> a field of study or a software product that doesn't provide enough >> documentation and tools for people to be self-sufficient. To clarify, I >> haven't played the fool in this context. >> >> So I had four forms of an axiom that I thought were logically equivalent. >> For my own reasons, I was going to axiomatize all four of them. However, >> being properly paranoid, I was trying to prove they were equivalent, which >> led to me trying to disprove what had been for me a basic logic error, >> which led to counter examples on both the theorem and its negation, which >> led to me understanding how free variables work. >> >> Thank you Nitpick, for automating the holding of my hand. >> >> theorem >> "~((A --> B --> A) --> (A <-> B))" >> nitpick[sat_solver=MiniSat_**JNI,timeout=172800,verbose,**user_axioms] >> (*Nitpick found a counterexample: >> Free variables: >> (A∷bool) = True >> (B∷bool) = True *) >> oops >> >> theorem >> "(A --> B --> A) --> (A <-> B)" >> nitpick[sat_solver=MiniSat_**JNI,timeout=172800,verbose,**user_axioms] >> (*Nitpick found a counterexample: >> Free variables: >> (A∷bool) = True >> (B∷bool) = False*) >> oops >> >> theorem >> "~(!A. !B.(A --> B --> A) --> (A <-> B))" >> nitpick[sat_solver=MiniSat_**JNI,timeout=172800,verbose,**user_axioms] >> (*Nitpick found no counterexample.*) >> by auto >> >> Regards, >> GB >> >> >> >> >> > > > -- > 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] Thanks Nitpick for actually answering a former, simple question***From:*Alfio Martini

**Re: [isabelle] Thanks Nitpick for actually answering a former, simple question***From:*Alfio Martini

**References**:**[isabelle] Thanks Nitpick for actually answering a former, simple question***From:*Gottfried Barrow

**Re: [isabelle] Thanks Nitpick for actually answering a former, simple question***From:*Alfio Martini

- Previous by Date: Re: [isabelle] substitution
- Next by Date: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Previous by Thread: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Thread: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Cl-isabelle-users September 2012 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