*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Fri, 14 Sep 2012 20:13:38 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5052B80A.8020805@gmx.com>*References*: <5052B80A.8020805@gmx.com>*Sender*: alfio.martini at gmail.com

> > Hi Gottfried, I was more than convinced by the following answer from Paulson, stated in a previous e-mail (assuming my simpler question subsumes the one you posed): 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. So, they do not get quantified, but they have the same "denotation" (that is to say, they are equivalent under all interpretations.) All the Best! On Fri, Sep 14, 2012 at 1:52 AM, Gottfried Barrow <gottfried.barrow at gmx.com>wrote: > Hello, > > I break this out so the simple point doesn't get lost in the noise I > created from the last thread. > > The question was: What's the difference between free variables and > universally quantified variables? > > A partial answer is: Free variables don't get quantified. > > The software gave me the answer to my question. Propositions, tautologies, > contradictions. When a formula with free variables is a tautology or a > contradiction, then it's equivalent to a quantified form of the same > formula. If it's not a tautology or contradiction, then there's no > equivalency. It's that simple, at least for my simple cases. > > The use of the phrase "free variable" is all over the place: > http://en.wikipedia.org/wiki/**Free_variables_and_bound_**variables<http://en.wikipedia.org/wiki/Free_variables_and_bound_variables> > > In the context of FOL, you have formulas with free variables, but then you > put them in other formulas in which the variables get bound: > http://en.wikipedia.org/wiki/**First-order_logic<http://en.wikipedia.org/wiki/First-order_logic> > > "A formula in first-order logic with no free variables is called > a*first-ordersentence <http://en.wikipedia.org/wiki/** > Sentence_%28mathematical_**logic%29<http://en.wikipedia.org/wiki/Sentence_%28mathematical_logic%29>>*. > These are the formulas that will have well-definedtruth values < > http://en.wikipedia.org/wiki/**Truth_value<http://en.wikipedia.org/wiki/Truth_value>>under > an interpretation." > > This wasn't a case where I needed to study any logic. The stuff I need to > study is not this basic, discrete math level logic. I was making the wrong > assumptions, and I also needed to sync up some vocabulary, and maybe have > my mind refreshed just a little on stuff I haven't used on a daily basis. > > If I'm still wrong, all I can do, when the documentation doesn't cover a > topic, is make conclusions based on what I get the software to do. The > theorems below gave me the data to say what I said above. > > If "free variables don't get quantified" is supposed to be obvious because > of "free variables", it isn't. I gave the quote above, plus I had asked the > question, and I never got a simple, authoritative answer saying, "Free > variables don't get quantified". > > Regards, > GB > > theorem --"(1)" > --"As a test case, I show a quantified and free form equivalency, for a > true > proposition that's a tautology." > "(A & B --> A) <-> (!C.!D.(C & D --> C))" > by auto > > theorem --"(2)" > --"I then negate the formula inside the quantified variables, to show that > a > false proposition works as well, when it's a contradiction." > "~(A & B --> A) <-> (!C.!D.~(C & D --> C))" > by auto > > theorem --"(3)" > --"I then try to show an equivalency with another proposition that is > neither a tautology or contradiction. A counterexample is found." > "(A | B --> A) <-> (!C.!D.(C | D --> C))" > --"Nitpick found a counterexample: > Free variables: > (A?bool) = True > (B?bool) = False" > oops > > theorem --"(4)" > --"It turns out, free variable formulas are propositions. So a free > variable > formula is a tautology if a quantified form of it is proved to be true. > Here > the software doesn't care that the LHS and the RHS is false." > "(!C.!D.(C | D --> C)) --> (A | B --> A)" > by auto > > theorem --"(5)" > --"Here, the LHS is not quantified in any way, shape, or form, so it can't > be > used to prove the RHS." > "(A | B --> A) --> (!C.!D.(C | D --> C))" > --"Nitpick found a counterexample: > Free variables: > (A?bool) = True > (B?bool) = False > Skolem constants: > (C?bool) = False > (D?bool) = True" > oops > > > -- 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] Free variables aren't quantified, it's that simple (by all appearances)***From:*Gottfried Barrow

**Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)***From:*Gottfried Barrow

**References**:**[isabelle] Free variables aren't quantified, it's that simple (by all appearances)***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)
- Next by Date: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)
- Previous by Thread: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)
- Next by Thread: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)
- 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