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
(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