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