Thanks for the interesting link. I do not understand Buzzard's comment:
"It's completely safe because every single *theorem* where division by 0
isn't allowed contains the hypothesis that the denominator isn't 0 in its
statement."
How can you enforce that in the future, someone will not write a theorem
not satisfying this ? Or is it again a "gentleman's agreement" ?
> The key insight is that because this does not affect consistency (it's a
>> definition)
>>
>> I don't understand: definitions like this may lead to inconsistencies
>> (for instance, here, you'd better avoid the axiom x x^{-1} = 1). The
>> theory of meadows is of course consistent, but in general, one has to be
>> careful. Or you were referring to something more specific ?
>>
>
> The point is that a definition has the form...
>
> I was reacting to Mario's "it does not affect consistency because it's a
definition". Maybe there is also a definition soundness check in Lean and
Mario meant "it does not affect consistency because this definition of
inversion passes the definition soundness check".
The "definition soundness check in Lean" is baked into the type theory.
> MM0's definition mechanism is a simplified version of Lean's: certain terms
> are marked as definitions, given values, and there is a conversion rule for
> unfolding a definition. Importantly, the "convertibility" or "definitional
> equality" judgment used for this purpose penetrates through *all* terms
> unconditionally. Metamath doesn't have definitional equality; we model it
> using = for classes and <-> for wffs, but for this to work we need equality
> theorems for *all* term constructors in the language, unconditionally.
> These have to be axiomatized for primitive term constructors like A. and
> e., but for definitions they can be proven provided you can unfold
> definitions unconditionally (which invalidates method 2).
>
Ok, so it's a definition in the sense of "passing the definition soundness
check", as I thought. All is good. I think the line "Cons" I wrote for
proposal 2 summarizes it faithfully with "not a definitional extension".
Thanks for making it clearer.
Benoît
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e2562fc8-e08f-484a-bc8b-421e32fd3ff0%40googlegroups.com.
