Re: [mizar] Re: reductions in Mizar

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

On 1/26/12, Freek Wiedijk <freek@cs.ru.nl> wrote:
> Jesse:
>
>>I would find it unpleasant if a the validity of a proof
>>depended on the confluence of a non-trivial reduction
>>relation whose confluence I didn't understand or to which
>>I had no direct access.
>
> This is more about termination than about confluence.  And
> even so, the _validity_ of the proof would depend on neither.
> The only thing that would depend on these kind of properties
> is the behavior of the checker.  Once it terminates and
> accept the proof, you would know you had a correct proof,
> no matter what the properties of the reduction relation.
>
> So the only thing that might not be obvious anymore if
> you allowed more complicated reductions would be that the
> checker will always terminate.
>
> Not that I propose to allow more involved reductions.
> Although people from the type theoretic community apparently
> consider this kind of automation in a checker very important.

I thought Gonthier (the only Coq person who recently turned to serious
math library building) is opposed to having such heavy machinery
inside the PA. For the same "fragility of refactoring" reasons as the
Mizar people have been taught to over a couple of decades.

Josef




>
> Freek
>