Re: Re: reductions in Mizar

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.

Freek