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

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

```
"A formula in first-order logic with no free variables is called a*first-ordersentence <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>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

```

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