*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 14 Sep 2012 22:30:34 -0500*In-reply-to*: <CAAPnxw2rN58zudM5Ti_TZfEFqYGeyVFxABNrruh-=_Z7AGkqqQ@mail.gmail.com>*References*: <5052B80A.8020805@gmx.com> <CAAPnxw2rN58zudM5Ti_TZfEFqYGeyVFxABNrruh-=_Z7AGkqqQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 9/14/2012 6:13 PM, Alfio Martini wrote:

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,

Alfio, You say, "assuming my simpler question subsumes the one you posed".

I was talking about free variables in the mere statement of a theorem, like, theorem --"(3)" "(A | B --> A)<-> (!C.!D.(C | D --> C))" oops

So, they do not get quantified, but they have the same "denotation" (that is to say, they are equivalent under all interpretations.)

Regards, GB

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

**Follow-Ups**:

**References**:**[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:*Alfio Martini

- 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