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

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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.