Re: [isabelle] Thanks Nitpick for actually answering a former, simple question
On 11.09.2012 22:07, Gottfried Barrow 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?"
For a free variable a not bound in any enclosing context, 'lemma "P a"'
is always equivalent to 'lemma "!a. P a"' in that each of these lemmas
can be derived from the other.
But the implicit all quantification happens on the outermost level of
the term, which explains your examples below. They can be simplified as
"~((A --> B --> A) --> (A <-> B))"
"!a b. ~(P a b)"
"(A --> B --> A) --> (A <-> B)"
"!a b. P a b"
"~(!A. !B.(A --> B --> A) --> (A <-> B))"
"~(!a b. P a b)"
This archive was generated by a fusion of
Pipermail (Mailman edition) and