[mizar] Re: Urelements?

[Jesse Alama <jesse.alama@gmail.com>]

I don't know exactly how the checker works, so this may be out of
line, but here is one simple idea that doesn't even use heuristics.
One could try a breadth-first approach to expansion: first don't do
any definitional expansion, and try running the inference through the
checker.  If that fails, uniformly expand once anything that could be
expanded, and retry the inference with a bigger premise set.  And so
forth.  That's how SAD, for example, handles definitions.  This
preserves the complete/exhaustive property of the checker.  This would
probably not deliver the big speedups that Artur finds when expansion
is switched off, but it might help nonetheless.  And with this
approach, one needn't to introduce a new primitive type.

Jesse

Josef Urban <josef.urban@gmail.com> writes:

> Calling the basic object of set theory an "element" and preventing its
> automated typing as "set" feels foundationally inventive.
>
> It seems that you want additional ad-hoc type/definitional-expansion
> machinery for some particular sets. I would not do it ad-hoc for two
> kinds of objects, but rather have a standard mechanism that allows to
> mark a definition as something that should not be automatically
> expanded by default (or in an environment). We faced a similar
> situation some time ago with quaternions, and that had nothing to do
> with foundations - just with having proper mechanisms for "knowledge
> expansion".
>
> Josef
>
> 2012/3/12  <trybulec@math.uwb.edu.pl>:
>> Let me make one thing clear:
>>
>> we do not propose to chang the foundations of MML. The chang eis rather
>> related to type handling.
>>
>> The (quite old/brand new) TARSKI:1 will be
>>
>> for x being element holds x is set
>>
>>
>> It now obvious that 2 is a set, I mean
>>
>>     2 is set;
>>
>> is accepted without any references. In new approach it will need
>> justification:
>>
>>     2 is set by TARSKI:1;
>>
>> I used many times (and it must be revised)
>>
>>     1-sorted(#1, ... #)
>>
>> for 1-element 1-sorted. I even wanted to do a revision :-). With new
>> approach
>> one must write
>>
>>     1-sorted(#{0}, ...#)
>>
>> that means the same and it less tricky.
>>
>> Regards,
>> Andrzej
>>
>>
>>
>>
>

--
Jesse Alama
http://centria.di.fct.unl.pt/~alama/