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



Thank you Paulson!

I was assuming that the only possibility would be this folklore
(convention). I feel more
relaxed now.

However, in your book (ML for the Working Programmer, chapter 6, Reasoning
about Functional
Programs) you are [to my personal taste] very careful, and
all the theorems are stated with proper quantification, albeit expressed in
[English]
metalanguage.

Only the application of existential and universal introduction rules are
left implicit (as
is common in usual mathematical prose).

All the Best!

On Wed, Sep 12, 2012 at 10:47 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

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


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