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


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:

"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".


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"

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"

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