Re: [isabelle] Schematic vars or universal bound vars in theorem?

This reply to my email is a basic logic fix, in case it matters to someone.

For my equality axiom, I was using something like this:

    (1) "!u. !v. !x. ((x <\in> u <-> x <\in> v) --> u=v)",

with a corresponding theorem like this:

    (2) "!u. !x. (~(x \<in> u)  -->  u = Sigma_E)".

The textbook formula came to my mind, so I changed the axiom to:

   (3) "!u. !v. ((!x.(x \<in> u <-> x \<in> v)) --> u=v)".

Which then required a corresponding change to my theorem to not get an error:

    (4) "!u. ((!x. ~(x \<in> u))  -->  u = Sigma_E)".

My questions about schematic vs. universal bound variables stay the same.


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