# [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.*