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
"!a b. ~(P a b)"
"!a b. P a b"
"~(!a b. P a b)"
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".
theorem "(!a. P a) <-> (!b. P b)" apply auto done
I want to make "b" a free variable so that I can prove, stated
"(!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
I can prove these two equivalent forms of a theorem, one with free
variables, and one with bound:
--"3 implications proves 3 propositions are equivalent."
"!A B C.(A --> B) & (B --> C) & (C --> A) <-> (A <-> B) & (A <-> C)
& (B <-> C)"
--"Now with free variables."
"(A --> B) & (B --> C) & (C --> A) <-> (A <-> B) & (A <-> C) & (B
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and