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