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