Re: [mizar] Urelements?

[Josef Urban <josef.urban@gmail.com>]

Hi Andrzej,

good first-order automated theorem provers today routinely prove facts
over the whole MML, particularly if they have reasonable guidance. But
if you just pull together hundreds of facts and feed them to the very
basic Mizar checker (which is just brute-force and has practically no
indexing), you will get what Artur got. Any other result would be very
surprising.

You can try to use the Mizar notion of type as a guidance for
definitional expansions. A very simple heuristic could watch that the
defining formula still talks about the types of the original objects.
But I am not sure I would want that in general. In large ontologies
(and Mizar's type system is fairly close to a large ontology), type
climbing is an essential proving method.

A more general method could allow to tell the checker: in this article
(environment), do/don't perform certain type climbing and do/don't
perform certain definitional expansion. That's what mathematicians do:
they hardly ever expand the definition of real numbers. But I don't
see how changing the current (relatively clean and well-designed) soft
type system to a combination of hard and soft will be more useful than
that.

It seems to me that there is quite a lot of confusion in formal
mathematics between "suitable foundations" and "suitable automation".
People who implement proof assistants are typically
logicians/mathematicians, so when they face an automation challenge,
they will proudly come up with their "new, (now perfect) foundations"
that "solve it all" (again), instead of just engineering good
automation for foundations that are already common and accepted by
others.

Best,
Josef


2012/3/11  <trybulec@math.uwb.edu.pl>:
> Hi;
>
> I would like to start with Polish "Nie przesadzajmy, jak mawiał leniwy
> ogrodnik", I do not know how to translate it. I wonder what Google does with
> it.
> It seems that we exaggerated with the statement that everything is a set.
> Actually numbers and structures behave rather like urelements (I am aware
>  that
> elements of structures are supposed to be urelements, not the structures
> themselves).
>
> In old Mizar the root type (and mode) was 'Any'. The type 'set' was a
> subtype of 'Any', the first axiom in TARSKI said that 'everything is a set'.
> One of the reason was that we planned to develop other repositories based
> e.g. on arithmetics, in which probably the first axiom would be 'everything
> is a natural number'. Then we decided that it is enough trouble with one
> MML, and keeping two different types with the same denotation is useless.
>
> Recently Artur started to experiment with definitional expansion of atomic
> sentences in the Inference Checker (CHECKER in the Mizar jargon) and the
> results are disgusting. Verifying some articles becomes longer by more than
> two orders. One of the reason was the lack of the type discipline. If e.g.
> 'x <> y' is among premises the poor thing will append to premises both 'not
> x c= y' and 'not y c= x' even when x and y are real numbers and such
> inclusions are (almost) meaningless.
>
> Therefore it is necessary to recover the old root type, under the new name
> 'element'. When identifying 'Any' and 'set' was easy, going back is a little
> bit harder. The first obvious step was done (by Czeslaw and Artur):
>
> i. in HIDDEN the mode 'element' is introduced and it is the mother type of
> the mode 'set'. The equality is introduced for elements, but the membership
> needs the second argument to be a set.
> ii. default types for numerals and structures are put to 'set' (temporarily)
> iii. when in the functor or mode definition qualification was empty, it was
> by default set, it was necessary, again for a while, to insert the
> qualification '-> set'.
>
> We should now discuss what should be a set, and what should not. E.g.
> ordered pairs are probably elements, not sets?
>
> Regards,
> Andrzej
>
>
>
>
>
>
>
>
>
>
>