[isabelle] Sledge and 0; green & blue; ATPs lovin' quantifiers


Embarrassing mistakes are embarrassing, but green and blue variables can help prevent them, at least if you don't tell others.

It's in the story below that I tell about going from vaguely noticing blue variables when I edit a formula, to discovering another great feature of jEdit, that green variables are bound variables and blue variables are free variables. Did I know that? If I did, I forgot it.

Color coded variables even help with respectable mistakes, like when I go through and change all my variables for a different naming convention.

Since starting this email, I noticed another blue variable that should've been green. Yet, in spite of the misnamed variable, the theorem was still true.

It's always a scary thought when Sledgehammer proves a theorem which isn't what I think it is.


(This is a tangent. I had led into it from the last section, but then I deleted a lot of the last section. It follows the general pattern of, "Dude, this is great stuff.")

In real life, there's the Axiom of Separation, which requires we use a set which already exists to create new sets, but most every one is oblivious to it.

Set theorists are a rare breed of people, but I know one who was a former professor. I emailed him and asked, "Trey, everyone is oblivious to the Axiom of Separation, which requires both an existing set and a property, but most people mindlessly only specify the property. How many proofs do you think are out there where they think they're using a set, but they're really using a class?"

He emailed me back a simple response. He said, "Well, most people are working in the big areas of math, like algebra and real analysis, so the sets they're using have been proved to exists, so those people are safe."

The great thing about formal proofs, as things are turning out, is that I can force the code to always require the explicit use of the Axiom of Separation.

Do you want to use my set builder notation? Then you have the choice of {A. P} or the more traditional notation {x IN A. P x}. Either way, you explicitly have to specify the set A that you're going to get your elements from, where A is tied into the axiom

   !A. !P. ?B. (!x. x IN B <-> (x IN A & P x)).


So for a simple example, I had,

  !q. empty_set not_in {x IN u. x notEq empty_set}

where "u" was blue. It turned out the same, since "q" wasn't used and "u" is a free variable, but it's definitely bad style.


Today, the blue variable awareness came because I ran Sledgehammer on an existence theorem. Like many times, multiple ATPs gave multiple results, where the axioms and theorems used by the different ATPs fell into groups.

First, here's the ATPs which regularly produce results for the FOL heavy theorems I'm doing:

    metis, vampire, e, spass_new, remote_e_sine, z3_tptp, and z3.

And frequent enough to notice:

    satallax, cvc3.

And not frequent, but not totally absent, like other ATPs:


Anyway, I think it was vampire which proved the existence of unordered pairs using only the existence of the empty set.

I said, "That's no good. What a classic mistake, to forget about the trivial case of the empty set."

I added the condition that my set is non-empty, and I had a "by(auto)" below them theorem, and auto proved the theorem after I edited it.

I said, "That's no good."

Well, I had made another classic mistake. There were two "z"s, where one was outside the scope of the quantifier, where it originally had been inside the scope.

It was at this point that I noticed one green "z" and one blue "z". I thought, "That Makarius, giving us green variables and blue variables, is that great, or what?"


This eventually tied into me trying to sort out some set notation.

From Set.thy, I got this the basic idea for this notation for my ordered pairs function, S_se :: "sT => (sT => bool) => sT":

    "{q. P}" == "CONST S_se q P"
    "{x : q. P_x}" => "{q. (%x. P_x)}"

This is simple stuff, but everything is hard until you understand it, so I was working through some examples where I was starting with the set builder notation, {x : q. P_z}, and translating into the two other equivalencies, where it's all related to the formula

!q. !z. z IN {x : q. P_x} <-> (z IN q /\ (%x. P_x) z) <-> z IN {q. P}.

One of the main things I was trying to explain was the relationship between P_x and P.

Basically, P_x is a first-order formula with a free variable x, so what happens if I make a mistake? And don't name my free variable x?

I worked up my trivial examples, the first being

    (1) theorem  "{0} = {x : {0}. x = 0}"
          by(metis singleton_as_a_separation_set),

where 0 is the empty set, and  P_x == (x = 0)

Now, my fluency in the Isar proof language is comparable to my fluency in Spanish, where I know how to say "by auto" and "by metis", along with "burrito", "taco", hombre, and adios. So I'm much more ahead in Spanish than I am in Isar, but I'm learning things about Isabelle that I need to learn anyway, and I'm not stuck now completely in tutorial purgatory.

Sledgehammer makes mincemeat out of (1), so I messed it up so there's a blue variable, y, which results in a false variation of (1):

    (2) theorem  "~(!y. {0} = {x : {0}. y = 0})"
          by(metis (mono_tags) Ax_P separation_set_uniqueness).

I put the quantifer in to show effectly what happens when my P_x == (y = 0), which results in no free variable x in P_x.

There was the lesson on remembering to consider the trivial case of the empty set.

There was the lesson of getting visual feedback to see if my variables are bound or free.

The third lesson had to do with my past question, up until today, of whether to leave a variable free, or make it a bound universally quantified variable.

This was no small question, and my inclination was to go through the formalities for a while of explicitly using universal quantifiers, and then loosening up and using free variables.

It's all the same, right?

No. All the ATPs above that easily proved (2) timed out on the version that has a free variable, which is this theorem:

    theorem  "~({0} = {x : {0}. y = 0})"

Maybe there's something I'm missing, but what I'm thinking is that the ATPs that are good at proving FOL, work best when they're given explicit FOL.

If that's what they want, who am I to deny them what they want? I do what I can to make ATPs happy, so they'll help me out.


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