# [isabelle] Thanks Nitpick for actually answering a former, simple question

```Hello,

```
It's not like I call up Bill Gates to learn about Windows 7, and if it sounds like I'm complaining, that would be a sound similar to complaining. I'm not complaining. I'm just talking because I'm allowed to.
```
```
Like two months ago, I specifically asked, in a fairly precise way, "What's the difference between free variables and universally quantified variables, and is there a reason I shouldn't use free variables?"
```
I will now give you a reasonably close, informal, one sentence answer.

```
ANSWER: A universally quantified bound variable is a logical statement, where a free variable is an argument to a function.
```
```
That's kind of huge difference don't you think? But two months ago, based on the zero answers like the above, I eventually started treating free variables like universally quantified variables.
```
Who straightened me out? Nitpick.

```
So I looked at the tutorials again, and "instantiation of free variables" became more clear. However, if I didn't write the software, how was I supposed to know how the proof engine is instantiating free variables when proving a theorem? Who's to say that it's not instantiating them in way that makes them equivalent to a universally quantified variable? Obviously not.
```
```
This substantiates my general guiding principle that it's a fool who picks a field of study or a software product that doesn't provide enough documentation and tools for people to be self-sufficient. To clarify, I haven't played the fool in this context.
```
```
So I had four forms of an axiom that I thought were logically equivalent. For my own reasons, I was going to axiomatize all four of them. However, being properly paranoid, I was trying to prove they were equivalent, which led to me trying to disprove what had been for me a basic logic error, which led to counter examples on both the theorem and its negation, which led to me understanding how free variables work.
```
Thank you Nitpick, for automating the holding of my hand.

theorem
"~((A --> B --> A) --> (A <-> B))"
nitpick[sat_solver=MiniSat_JNI,timeout=172800,verbose,user_axioms]
(*Nitpick found a counterexample:
Free variables:
(A∷bool) = True
(B∷bool) = True *)
oops

theorem
"(A --> B --> A) --> (A <-> B)"
nitpick[sat_solver=MiniSat_JNI,timeout=172800,verbose,user_axioms]
(*Nitpick found a counterexample:
Free variables:
(A∷bool) = True
(B∷bool) = False*)
oops

theorem
"~(!A. !B.(A --> B --> A) --> (A <-> B))"
nitpick[sat_solver=MiniSat_JNI,timeout=172800,verbose,user_axioms]
(*Nitpick found no counterexample.*)
by auto

Regards,
GB

```

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