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

>However, in your book (ML for the Working Programmer, chapter 6, Reasoning about Functional >Programs) you are [to my personal taste] very careful I mean this in the most positive way possible! On Wed, Sep 12, 2012 at 10:47 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > 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 > > -- 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

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

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

- Previous by Date: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Date: Re: [isabelle] Parallel proofs issue, potentially in subst method
- Previous by Thread: Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
- Next by Thread: [isabelle] Comparing two graphs
- 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