[isabelle] Thanks Nitpick for actually answering a former... · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Thanks Nitpick for actually answering a former...

Email Gateway (Aug 19 2022 at 08:46):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
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

Email Gateway (Aug 19 2022 at 08:46):

From: Lars Noschinski <noschinl@in.tum.de>
On 11.09.2012 22:07, Gottfried Barrow wrote:

Hello,
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?"
[...]
For a free variable a not bound in any enclosing context, 'lemma "P a"'
is always equivalent to 'lemma "!a. P a"' in that each of these lemmas
can be derived from the other.

But the implicit all quantification happens on the outermost level of
the term, which explains your examples below. They can be simplified as
follows:

theorem
"~((A --> B --> A) --> (A <-> B))"

"!a b. ~(P a b)"

theorem
"(A --> B --> A) --> (A <-> B)"

"!a b. P a b"

theorem
"~(!A. !B.(A --> B --> A) --> (A <-> B))"

"~(!a b. P a b)"

-- Lars

Email Gateway (Aug 19 2022 at 08:46):

From: Lawrence Paulson <lp15@cam.ac.uk>
I really don't understand what you mean. Bound variables are not logical statements. And whether a variable is free or bound has no bearing on whether or not it can appear as a function's argument.

Larry Paulson

Email Gateway (Aug 19 2022 at 08:47):

From: Lars Noschinski <noschinl@in.tum.de>
On 11.09.2012 22:07, Gottfried Barrow wrote:

Hello,
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?"
[...]
For a free variable a not bound in any enclosing context, 'lemma "P a"'
is always equivalent to 'lemma "!a. P a"' in that each of these lemmas
can be derived from the other.

But the implicit all quantification happens on the outermost level of
the term, which explains your examples below. They can be simplified as
follows:

theorem
"~((A --> B --> A) --> (A <-> B))"

"!a b. ~(P a b)"

theorem
"(A --> B --> A) --> (A <-> B)"

"!a b. P a b"

theorem
"~(!A. !B.(A --> B --> A) --> (A <-> B))"

"~(!a b. P a b)"

-- Lars

Email Gateway (Aug 19 2022 at 08:47):

From: Tjark Weber <webertj@in.tum.de>
I believe a more helpful insight here is simply that a formula with
free variables may be contingent (i.e., its truth value may depend on
the interpretation of the free variables, so that neither the formula
nor its negation are theorems), while a formula without free variables
is either true or false.

See http://en.wikipedia.org/wiki/First-order_logic (especially the first
three sections) for further background.

Best regards,
Tjark

Email Gateway (Aug 19 2022 at 08:47):

From: Alfio Martini <alfio.martini@acm.org>
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@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

Email Gateway (Aug 19 2022 at 08:48):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Email Gateway (Aug 19 2022 at 08:48):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Lars,

And Makarius had talked some about outermost quantifiers in an email,
and how they get stripped away.

Using Isabelle as a logic calculator, the basic idea is, "GB, with your
logic calculator, check yourself compulsively on the most basic of logic
ideas, before claiming what is wrong. They will be embarrassed for you."

However, I didn't have utmost confidence that, for the free variable
formula, there was an equivalent formula with bound variables, and that
I just needed to discover the rules, because I thought Nitpick had
taught me the rules, when all it had done was slap my hand.

In this case, my logical calculator doesn't help me use trial and error,
with a little understanding, to prove the equivalency of a "free
variable formula" with its equivalent "bound variable formula".

Consider:

theorem "(!a. P a) <-> (!b. P b)" apply auto done

I want to make "b" a free variable so that I can prove, stated
informally here,

"(!a. P a) <-> (P b)"

But once I make "b" free, I explicitly end up with,

theorem "!b. (!a. P a) <-> (P b)" apply auto oops

My logic calculator can never show me how free variables are implicitly
quantified. I just have to know. (I get in trouble when I make emphatic
claims.)

I can prove these two equivalent forms of a theorem, one with free
variables, and one with bound:

theorem
--"3 implications proves 3 propositions are equivalent."
"!A B C.(A --> B) & (B --> C) & (C --> A) <-> (A <-> B) & (A <-> C)
& (B <-> C)"
by auto

theorem
--"Now with free variables."
"(A --> B) & (B --> C) & (C --> A) <-> (A <-> B) & (A <-> C) & (B
<-> C)"
by auto

But I can't use the safety net of mechanized proofs to make sure that
I'm using free variables the way I think I'm using them, which I would
do, even if something looked obvious.

If you say, "You've proved they're equivalent," then I say, "No, I've
only proved that they're both true." I have to take your word for it
that, in the software, they are logically equivalent.

Oh, well. Faith is required when I can't read the source code.

Thanks for the help.

Regards,
GB

Email Gateway (Aug 19 2022 at 08:48):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Tjark,

I think I'm straightened out, but the least little difference in what
people say can make me wonder if I'm straightened out.

I think what confused me is that I was assuming that how Nitpick uses a
formula in a theorem, such as,

theorem "~((A --> B --> A) --> (A <-> B))"
oops

is the same way the prover engine uses it. (I still wouldn't know what
the software is doing.)

If you had said before my email, "GB, the truth value of '~((A --> B -->
A) --> (A <-> B))' cannot be determined until you assign truth values to
A and B", then at worst, I would have said, "Tjark, I remember that now.
I used to be so good at thinking in terms of truth tables before
Isabelle started overloading me with information."

Anyway, I always get a little extra out of these exchanges, even if I
don't start them off right.

Whatever is actually happening in Nitpick's engine and the provers
engine, I now know that with free variables, I can consider that Nitpick
is checking a "theorem" like this:

definition false_formula::"bool => bool => bool" where
"false_formula A B == ~((A --> B --> A) --> (A <-> B))"
value "false_formula True True" (*Output panel: "False" :: "bool" *)

That helps a lot, because I was in this mindset that when Nitpick found
counterexamples for both a "theorem" and its negation, that it had found
an inconsistency.

On the other hand, I now consider that the prover engine has converted
my theorem above to

theorem "!A B. ~((A --> B --> A) --> (A <-> B))"
oops

even though Makarius has talked about quantifiers getting stripped away.

Thanks for the help,
GB

Email Gateway (Aug 19 2022 at 08:48):

From: Alfio Martini <alfio.martini@acm.org>
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!

Email Gateway (Aug 19 2022 at 08:48):

From: Alfio Martini <alfio.martini@acm.org>

However, in your book (ML for the Working Programmer, chapter 6, Reasoning
about Functional
Programs) you are [to my personal taste] very careful

I mean this in the most positive way possible!

On Wed, Sep 12, 2012 at 10:47 AM, Lawrence Paulson <lp15@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@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@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

Email Gateway (Aug 19 2022 at 08:49):

From: Makarius <makarius@sketis.net>
This was about the Pure connectives !! and ==> which are not the same as
HOL ! and --> (and more), even though sometimes people prefer to smash
that distinction. The point of Pure connectives is to describe the
structure of a rule statement declaratively, so that the system knows what
is meant and how to compose the rules (by back-chaining and unification).

This is in contrast to the usual FOL view on logic with many connectives,
and application-specific operations (set-theory, lattices etc.).
Automated tools turn all this object-logic material and the Pure !! and
==> into hash-brown, and try to serve that to the user. This often works,
but is no longer Pure logic, the one underlying Isar proofs.

So when you state

lemma "!x y. A x --> B y"

your result is again compact "!x y. A x --> B y" (with its implicit
Trueprop wrapping).

But when you state

lemma "!!x y. A x ==> B y"

your result is schematic "A ?x ==> B ?y". You can get the same rule by
writing the statement with explicit "eigen-context" as follows:

lemma fixes x y assumes "A x" shows "B y"

lemma assumes "A x" shows "B y"

in most situations, where x and y are implicitly free and thus ready to be
fixed at the outermost level.

In the latter two forms, the resulting rules emerge naturally, without
navigating through logical connectives first.

Makarius

Email Gateway (Aug 19 2022 at 08:49):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
(This reply never come back to me, and it's been hours since 2 other
emails came back that were sent out later. I made a few edits.)

On 9/11/2012 3:55 PM, Lawrence Paulson wrote:

I really don't understand what you mean. Bound variables are not
logical statements. And whether a variable is free or bound has no
bearing on whether or not it can appear as a function's argument.

Larry, I was only saying that if I have a variable x, and I say "for
every x", then it's an informal statement saying that something is true
for every x, where formally, "for every x" is, of course, not a
well-formed formula.

Your question is about logic, not Isabelle.

It's not that I don't make the most basic of mistakes, but once Nitpick
tells me that (P x) is used differently than (!x. P x), I stop assuming
anything but what I've explicitly been told. I don't subscribe to
"assume the obvious".

...It is a convention in logic that any theorem involving free
variables denotes the "universal closure" of that formula...

But it's not convention that a "theorem" formula is also a function that
can be called with arguments. Convention has it that theorems are
symbols on a piece of paper, or in a PDF, probably generated by LaTeX.
That's the world I come from. When it comes software, it's best to know
explicitly what is implicitly stated.

I might have eventually discovered my misunderstanding of basic logic,
but I jumped to conclusions when I saw that Nitpick treats a false
formula with free variables different than an equivalent false formula
with bound variables.

(1) theorem "~((A --> B --> A) --> (A <-> B))", is disproved with free
variables True and True.

(2) theorem "!A.!B.~((A --> B --> A) --> (A <-> B))", is disproved with
Skolem constants True and True.

By all appearances, (1) is being disproved by using the formula as a
function, and (2) is being disproved differently. I don't know. Nitpick
doesn't tell me, and I'd hate to email Jasmin asking for details.

I've never read in the documentation how to make the quantification of
free variables explicit, only that free variables become schematic
variables. So when I saw formulas being called as functions, and it
wasn't me calling them, then the result was that I only understood.

I don't know that it could have been any different, unless maybe a
couple of months had passed for me to think about it and experiment.

"Theorem" formulas also being functions is a new game, and on my own,
using trial and error, I was reduced to using Isabelle as a logic
calculator (a very important use for it) to try and figure what the
rules are.

Information overload can lead to misunderstanding, but assuming the
supposedly obvious is no good either. It's better to be told explicitly
the rules. This rule could be there somewhere in the documentation.
There's a whole lot to read that I haven't read.

I'm not actually using theorems as functions which take arguments, so I
don't know the details of passing values.

Your software has so many features, it's taking me a long time to get to
them all, especially if I've started to use the software after only
learning a few features. And someone like me has a tendency to jump to
many intermediate conclusions, some partially right, some partially
wrong, many totally wrong, and periodically, some totally right.

Regards,
GB

On 11 Sep 2012, at 21:07, Gottfried Barrow<gottfried.barrow@gmx.com>
wrote:

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.

Email Gateway (Aug 19 2022 at 08:49):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 9/11/2012 3:55 PM, Lawrence Paulson wrote:

I really don't understand what you mean. Bound variables are not logical statements. And whether a variable is free or bound has no bearing on whether or not it can appear as a function's argument.

Your question is about logic, not Isabelle.

...It is a convention in logic that any theorem involving free variables denotes the "universal closure" of that formula...

But it's not convention that the statement of a theorem/conjecture is
also a function that can be called with arguments.

(1) theorem "~((A --> B --> A) --> (A <-> B))", is disproved with free
variables True and True.

(2) theorem "!A.!B.~((A --> B --> A) --> (A <-> B))", is disproved with
Skolem constants True and True.

I've never read in the documentation how to make the quantification of
free variables explicit, only that free variables become schematic
variables. So you throw in that formulas act as functions, and through
trial and error, I only discovered what I shouldn't do. I don't know
that it could have been any different, unless maybe a couple of months
had passed to think about it and experiment.

Theorem/conjecture formulas also being functions is a new game, and on
my own, using trial and error, I was reduced to using Isabelle as a
logic calculator (a very important use for it) to try and figure what
the rules are.

I'm not actually using theorems as functions which take arguments, so I
don't know the details of passing values.

Your software has so many features, it takes me long time to get to them
all, especially if I've started to use the software after only learning
a few features. And someone like me has a tendency to jump to many
intermediate conclusions, some partially right, some partially wrong,
many totally wrong, and periodically, some totally right.

Regards,
GB

On 11 Sep 2012, at 21:07, Gottfried Barrow<gottfried.barrow@gmx.com> wrote:

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.

Last updated: Nov 21 2024 at 12:39 UTC