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



Your question is about logic, not Isabelle.

The formula (?x + ?y) + ?z = ?x + (?y + ?z) expresses a property about three quantities denoted by ?x, ?y and ?z. It is a convention in logic that any theorem involving free variables denotes the "universal closure" of that formula, here

"all x. all y. all y. (x+y)+z =  x + (y+z)".

Isabelle is designed to work best a minimum of logical symbols, hence the preference for stating theorems like

	P1 ==> … Pn ==> Q.

Hardly any mathematics paper states such theorems as

	!x1 … xm. P1 & … & Pn —> Q.

Larry Paulson


On 11 Sep 2012, at 23:26, Alfio Martini <alfio.martini at acm.org> wrote:

> Dear Isabelle users
> 
> 
>> 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?"
> 
> Whenever I see this kind of discussion I remember that I am  actually
> interested in  the (logical ) difference [in Isabelle]
> between unknown variables and universally quantified variables,
> 
> For instance, the different roles of variables in the following    two
> propositions :
> 
> all x. all y. all y. (x+y)+z =  x + (y+z)
> 
> and
> 
> (?x + ?y) + ?z = ?x + (?y + ?z).
> 
>> From what I read, the operational meaning of the second matches the
> semantics of the first. But from a logical point of view, in the second
> proposition the variables are free, while in the first they are bound,
> so I get confused about it. I believe I "understand" this,  but then reality
> strikes and I think "who am I kidding"?
> 
> Cheers
> 
> On Tue, Sep 11, 2012 at 5:07 PM, Gottfried Barrow
> <gottfried.barrow at gmx.com>wrote:
> 
>> 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
>> 
>> 
>> 
>> 
>> 
> 
> 
> -- 
> Alfio Ricardo Martini
> PhD in Computer Science (TU Berlin)
> Associate Professor at Faculty of Informatics (PUCRS)
> Coordenador do Curso de Ciência da Computação
> Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
> 90619-900 -Porto Alegre - RS - Brasil






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