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