THE vs. SOME

7 views
Skip to first unread message

Victor Porton

unread,
Mar 6, 2009, 4:25:44 PM3/6/09
to vdash
The following theory verifies without errors

theory embedding
imports ZF
begin
definition "ZZZ == ( THE x. x = 0 )"
end

It however ceases to work when I replace THE with SOME. How we can
live without SOME?! I need some solution to use in place of SOME or to
make SOME work. Or maybe THE will work in the case when there are more
than one value? Will it?

Slawomir Kolodynski

unread,
Mar 6, 2009, 5:35:35 PM3/6/09
to vd...@googlegroups.com

Indeed, it looks like SOME is not supported in Isabelle/ZF. You may want to make sure by asking on the Isabelle mailing list.
I have done quite a lot of proofs in Isabelle/ZF and I have never needed SOME. Can provide a small example of how you would use SOME if it worked?
Maybe I will come up with some other approach that is sufficient for what you want to do.

THE is only usable when you have uniqueness.

Slawekk

--- On Fri, 3/6/09, Victor Porton <por...@narod.ru> wrote:

Reply all
Reply to author
Forward
0 new messages