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:
An answer to what question? What algorithm do you mean? And how do you relate this article to the topic of "free/bound variables"?

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


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.


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.


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.

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:


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.


Attachment: Universal instantiation and generalization.jpg
Description: JPEG image

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