Definition by existence

[Victor Porton]

I'm an Isabelle novice.

Let there is therorem "exists X such that P(X)". I want to define Y as
arbitrarily chosen (fixed) X confirming to this theorem.

What is the syntax for this?

[hen...@topoi.pooq.com]

On Tue, Feb 24, 2009 at 07:41:44AM -0800, Victor Porton wrote:
>
> I'm an Isabelle novice.
>
> Let there is therorem "exists X such that P(X)". I want to define Y as
> arbitrarily chosen (fixed) X confirming to this theorem.

Would being able to use this notation be equivalent to the axiom of
choice?

-- hendrik

[slawekk]

> Let there is therorem "exists X such that P(X)". I want to define Y as
> arbitrarily chosen (fixed) X confirming to this theorem.
>
> What is the syntax for this?

Let's say the theorem "exists X such that P(X)" is called my_theorem.
Then you can say in some proof:

obtain Y where "P(Y)" using my_theorem by auto

From that point on you can refer to the set Y and its property P(Y) in
this proof. This type of reasoning does not require the axiom of
choice.

[Victor Porton]

24.02.09, 20:33, "slawekk" <skok...@yahoo.com>:

As far as I understand, "obtain" can be used only in proofs.

I want something similar to "obtain" but in definitions (outside of proofs).

[slawekk]

>
> I want something similar to "obtain" but in definitions (outside of proofs).

If you had uniqueness you could use the "THE" keyword. Something like:

definition
"Q \<equiv> THE Y. P(Y)"

I used it a couple of times, although I prefer different ways of
getting the only set satisfying a predicate.

Since you don't have uniqueness you may check the similar SOME
construct.

definition
"Q \<equiv> SOME Y. P(Y)"

It might be what you want but I have never used it so I am not sure.