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


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.