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



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.