Re: [mizar] weak types

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

Andrzej:

>So, we have to distinguish carefully two things:
>-   using non standard definitions for well known concepts
>    (such as 'Element of A' )
>-   using permissiveness that means basically using some
>    form of Choice

Slightly related to this:

I would like to experiment with a Mizar-like system where the
rules of the logic are such that you will get extra proof
obligations (like PVS' TCCs) that guarantee that the meaning
of a function "outside its domain of well-definedness" will
never matter.

To give the foundations for such a system was the goal of my
paper with Jan Zwanenburg at TPHOLs this year.

As an example of what such a system would look like:
If you would have a proof with a step

	...
	A1: sqrt x > a by ...;
	...

then the justification would not only have to justify the
statement itself, but also the "assumptions of the functors"
(in this case "x >= 0").

>I do not believe that talking about "square circles" is
>intuitive.

No.  But Element of {} for me _is_ intuitive.  I still think
it's crazy (or at least: strange) that

	for x being Element of X holds ...

is not equivalent to

	for x being set st x in X holds ...

So "square circle" is not intuitive also because it is not a
dependent type.  If a mode can have parameters empty types
("weak types") become much more natural.  That's why I find
the non-emptiness of the HOL types less irritating that that
of the Mizar types.

I sometimes think that MML would have less "non empty"s in
the phrasing of the theorems if "Element of" would not behave
exceptionally for the empty set, as it is now the case.

Freek