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 well-formed formula.

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>  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 MHonArc.