*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*: Sun, 16 Sep 2012 12:00:26 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5053F65A.7060309@gmx.com>*References*: <5052B80A.8020805@gmx.com> <CAAPnxw2rN58zudM5Ti_TZfEFqYGeyVFxABNrruh-=_Z7AGkqqQ@mail.gmail.com> <5053F65A.7060309@gmx.com>*Sender*: alfio.martini at gmail.com

Hi Gottfried, You say, "assuming my simpler question subsumes the one you posed". > I'm pretty sure it doesn't. Please notice that I never use the schematic > variable notation, whereas you and Larry do. You are right, I missed that. For (3), I now call the left-hand side a proposition, and I think of it in > terms of propositional logic. I call the right-hand side a closed formula, > and I think of it terms of first-order logic. A proposition does not > necessarily have a definite truth value, whereas a closed formula does I understand that a proposition is the same thing as sentence, as it is often called and thus has to have a definite logical truth-value. In this way, I always comeback to the definition of interpretation. In first-order logic an interpretation assigns meanings only to the syntactic entities [of the signature or basis]. Meaning of free variables are fixed by the notion of a state, i.e., a function from variables to values. So, in first-order logic, any formula that contains [for instance] a free-variable "x" it is not [be called] a proposition, and it is actually a function(al) on that free-variable. It can be seen as having the type State=>Bool, where State is a function Vars=>D, Vars is the set of variables used to build the set of well-formed formulas and D is the domain in question. In this sense, the truth-value of this formula is open. It depends on the value of this free variable. It does not assert anything. Now, propositional logic is just a sublogic of first-order logic, with no function symbols and where all predicate symbols have arity zero. The "variables" here are just predicates. Thus, it is enough to fix an interpretation for these predicates in order to have the definite truth-value of the expression. So, from this point of view, every well-formed expression in propositional logic is a assertion, i.e., a sentence. That is why, I think, it can be called propositional or sentential logic. I am not sure if this view (as written above) is shared by other people, though. All the Best! On Sat, Sep 15, 2012 at 12:30 AM, Gottfried Barrow <gottfried.barrow at gmx.com > wrote: > 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'm pretty sure it doesn't. Please notice that I never use the schematic > variable notation, whereas you and Larry do. > > (On that email, it was to you, but I replied to Larry as if it was to me, > which I thought it was, but I apologize for that.) > > I've been asking about the relationship between free variables and > quantified variables in a formula prior to the formula being proved > (although some of my tangents involved proofs). I think you and Larry are > talking about formulas that have been proved. > > It might be so obvious to people that free variables don't get quantified > that everyone thought I was talking about post-proof free variables in a > proved theorem. > > First-order logic polluted my mind. I had the idea that any free variable > in P gets implicitly bound by the prover engine when I put P in the > statement `theorem "P"`. It makes sense now that it wouldn't. Propositions > are more general than closed formulas. > > According to the tutorial, free variables get converted to schematic > variables after a proof (page 7 tutorial.pdf). There is "free variable" > pre-proof, and "free/schematic variable" post-proof. > > 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 > > For (3), I now call the left-hand side a proposition, and I think of it in > terms of propositional logic. I call the right-hand side a closed formula, > and I think of it terms of first-order logic. A proposition does not > necessarily have a definite truth value, whereas a closed formula does. > That's what I showed below with my 5 examples. > > > So, they do not get quantified, but they have the same "denotation" (that >> is to say, they are equivalent under all interpretations.) >> > > So you would appreciate Larry's explanation more than me because I don't > know anything about interpretations. My interpretation is that everything > resolves to a boolean value of either true or false, based on my basic > understanding of logical connectives and quantifiers. > > 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> >>> <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> >>> <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/**<http://en.wikipedia.org/wiki/**> >>> Sentence_%28mathematical_****logic%29<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> >>> <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

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

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

- Previous by Date: Re: [isabelle] Eliminating two quantifiers in structural proof
- Next by Date: Re: [isabelle] Code generation for sorts from locales
- 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