Email Gateway (Aug 19 2022 at 08:44): Email Gateway (Aug 19 2022 at 08:44):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
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.
FORMAL PROOFS FORCING THE EXPLICIT USE OF THE SEPARATION AXIOM
(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)).
BACK TO THE BLUE VARIABLE
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.
NON-EMPTY SETS & SLEDGE NOT MAKING THE CLASSIC HUMAN MISTAKE
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:
yices.
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?"
A BLUE VARIABLE EXAMPLE ANSWERS A FORMER QUESTION
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.
*
THIRD BIG LESSON: FIRST-ORDER ATPs WANT FIRST-ORDER LOGIC*
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.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:44):From: Gottfried Barrow <gottfried.barrow@gmx.com>
This has occurred to me. That the reason the ATPs may not be able to
prove the theorem with the free variable, rather than the universally
quantified variable, is because all my previous theorems are done with
universal quantifiers rather than free variables.
To find out if that's true, I would need to change all the theorems so
that they use free variables.
Regards,
GB
Last updated: Nov 21 2024 at 12:39 UTC