Re: [isabelle] Thanks Nitpick for actually answering a former, simple question



On 9/11/2012 3:51 PM, Lars Noschinski wrote:
But the implicit all quantification happens on the outermost level of the term, which explains your examples below. They can be simplified as follows:
"!a b. ~(P a b)"
"!a b. P a b"
"~(!a b. P a b)"

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.