# Re: [isabelle] Happy New Year with Free/Bound Variables

On 1/3/2013 10:43 PM, Christian Sternagel wrote:

(Not having slipped this in anywhere else in the past, I got a
definitive, precise answer on the HOL4 list from Josef Urban by means of
this wiki article and his short example of how to use the algorithm
given in the article:
https://en.wikipedia.org/wiki/Extension_by_definitions

`An answer to what question? What algorithm do you mean? And how do you
``relate this article to the topic of "free/bound variables"?
`

Christian,

`If I wouldn't have wrote the last email, that wouldn't have been a bad
``thing.
`

`Anything I say more can be interpreted overall as me saying, "Hey,
``thanks all you developers for a great product. It's like the World Wide
``Web and the Internet, and technology in general. The newness can wear
``off, but I sometimes I still get that feeling again of 'this is awesome'".
`
HOW DO I RELATE IT TO...? (PART 1)

`The article, as part of an answer by Josef, is related to my tangent in
``my last email. There is "trying to prove your point logically", and then
``there are "facts". Facts, once I'm aware of them, can change a whole lot
``of things, motivation being one of them.
`

`You and Josef gave me facts. Prior to your example showing conclusively
``that implicit quantification is happening in Isabelle for free
``variables, Andrej's blog post might have put me in the "Hmmm, this has
``me worried. I need to think about this a whole lot to understand all of
``this."
`

`But now, knowing the fact that implicit quantification is happening in
``Isabelle, I say, "Well, Andrej, you say it's bad for people to say 'a
``free variable is implicitly universally quantified', but with Isabelle,
``they don't just say it, they go a step further and, for all practical
``purposes, hardwire that concept in the code, at least for the logic that
``would apply to the examples in your post, which would be first-order
``logic. As to there being any problems and limitations with doing that, I
``don't know what those would be. Others can fight those battles if there
``are battles that need to be fought."
`

`In the last email, I said his discussion is a different discussion, but
``surely it's still related. In his "Reason 6", he's making a big deal
``about us needing to be able to do a "Universal Generalization" proof,
``that is, by starting out with a arbitrary but fixed element of the real
``numbers, which, according to him, must be free, as represented by his
``"Consider any x /in R".
`

`(Here, I may sound like I know that I know what I'm talking about, but
``what I actually know is that I occasionally make a good point, but,
``otherwise, am very wrong much of the time. I also attached a pertinent
``image from Bloch's "Proofs and Fundamentals". I love even basic books
``like that, but I wish my formal education would have started me out at a
``lower level, so I wouldn't have wasted so much time on discovery.)
`

`So the facts you and Josef have given me have changed the nature of
``certain debates.
`

`That Andrej is making a valid point, I assume he is. That I can learn
``something from him, well, I have learned something from his Epilogue,
``which basically tells me what Bloch's book tells me, that Universal
``Instantiation is equivalent to Universal Generalization, but by him
``saying it, it drives home a point that otherwise wouldn't have gotten
``driven home, especially because of our recent Isabelle "implicit
``quantification" discussion.
`
But back to facts and their value.

`Adrej is getting dogmatic, which might have made me want to get dogmatic
``with him, but now I know certain facts, and I say, "Andrej, your
``discussion is ill-defined anyway. The Isabelle proof assistant has exact
``meaning in every statement we can make, and it could be that Isabelle's
``'Consider any x \in R' just becomes part of a big conjunction, which
``means we aren't truly doing a Universal Generalization proof. If we
``can't, then we can't. I'm not worried about it. Whatever the case, with
``Isabelle, there's something there rock solid to crtitique and attack if
``there's a problem."
`

`The last sentence was part of my "Hey, developers. Is Isabelle a great
``product, or what?" That the complement might come at some other people's
``expense, that can happen, and I touch on that below.
`
HOW DO I RELATE IT TO...? (PART 2)

`Mentioning the wiki article was a way to say something good about the
``people that contribute to the HOL4 mailing list, rather than to wait for
``some unlikely future date in which my complement would be completely on
``topic.
`
AN ANSWER TO WHAT QUESTION?

`Here, if I didn't give you this link, that wouldn't be a bad thing, but
``there is some good information in the thread, in particular, the
``culmination of it all for me in which Josef gives me the Wiki link, and
``enough of an explanation that I was able to figure out the rest on my own.
`
http://sourceforge.net/mailarchive/forum.php?set=custom&viewmonth=201209&viewday=&forum_name=hol-info&style=ultimate&max_rows=100&submit=Change+View

`The eventual, precise question was, "Can you give me a first-order
``formula which uses no constants for the formula 'the empty set is in the
``empty set'".
`
The very precise answer was given by Josef here:
http://sourceforge.net/mailarchive/forum.php?thread_name=CAFP4q17T2pEZhzXc5L5t9-kWuOLkVVbxNPEQt-WZGp%3DHG_gCsw%40mail.gmail.com&forum_name=hol-info
WHAT ALGORITHM DO YOU MEAN?

`The algorithm that Josef demonstrates when he converts "0 \in 0" to a
``FOL formula which only uses variables.
`

That I didn't learn about it from those other
group of people is a bad mark against them.

What is that supposed to mean?

`And if I didn't explain the meaning of that statement, it wouldn't be a
``bad thing. After all, to bash this other group of people on this mailing
``list is in bad taste.
`

`However, this other group of people is the group of people from which I
``got my formal education and looked to for answers after getting my
``degree, where my formal education is a B. S. in math. "Group" would mean
``mathematicians as a whole. I don't actually have any substantial
``complaints about those mathematicians who were my professors.
`

`My particular comment is related to the fact that in set theory books,
``I've repeatedly read that "in principle" we could do all set theory
``using first-order formulas, but we don't because it's way too
``impractical to actually do any of that, even just a little.
`

`I accepted that at face value, until I learned just enough first-order
``logic to start getting serious about learning axiomatic set theory. At
``that point, I started to challenge their "in principle" statement
``because I started to see that first-order logic needs to immediately be
``supplemented as a language to be used.
`

`I thought that there had to be symbols in the first-order logic
``specification to allow us to define constant symbols. Josef showed me I
``was wrong.
`

`Why didn't I learn that from that other group of people? At the bedrock
``of ZF sets is the requirement that zero constants are given to us.
``That's not little. That's huge. The FOL specification allows constants
``to be given in a FOL language, but none are given to us, and
``immediately, after the first ZF axiom, set theorists start introducing
``constants. Now, after knowing what I'm looking for, I can see that a few
``mention it, but what's in the Wiki article doesn't appear to be the
``common knowledge that it should be.
`

`I stop here, but I have a certain amount of cynicism about that other
``group. I can find ways to thank them later, but what have they done to
``help me be independent and get proof review? Nothing.
`
Regards,
GB

**Attachment:
**`Universal instantiation and generalization.jpg`

*Description:* JPEG image

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