Re: [mizar] structures

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>It cannot be related to the proof of a registration of an
>existential cluster, proofs are not exported, and then not
>imported either.

It is typical of constructive mathematics that the proof of
an existential statement is in one-to-one correspondence to a
specific object that has the property.  So this idea I had
just shows that I've been doing constructive mathematics too
much.

Now that I think of it, I expect that lassically it doesn't
make sense (what if you prove the existential by
contradiction?), and of course Mizar is a classical system.
So it probably is a bad idea anyway (even if you ignore the
import/export structure of the Mizar system) to relate "the
fixed theta" to the proof that theta is inhabited.

Sorry for the noise.

Freek