Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
(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
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
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.
On 11 Sep 2012, at 21:07, Gottfried Barrow<gottfried.barrow at gmx.com>
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and