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

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

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:

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