In the specific case of df-riota, Quine's definition 8.18 is equivalent
(see ~ dfiota2), and he mentions (p. 56) he designed it to evaluate to (/)
when there isn't unique existence, in particular so that the definition
remained a set for all possible arguments. So we are exactly following the
practice of at least one well-regarded authority.
On Sunday, January 12, 2020 at 6:09:52 PM UTC-5, Norman Megill wrote:
>
> On Sunday, January 12, 2020 at 5:24:59 PM UTC-5, Benoit wrote:
>>
>> On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:
>>
>
> ...
>
>
>> > 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 ?
>>
>
> There will never be an axiom x x^{-1} = 1) because the only axioms we use
> are the axioms of ZFC. (OK, you could artificially add new axioms and
> arrive at a contradiction, but the "This theorem was proved from axioms"
> list will quickly reveal that you're cheating.) The "axioms" we use for
> complex numbers are previously proven as theorems that are restated as
> axioms for convenience, but there still is nothing beyond ZFC.
>
> Definitions can never lead to inconsistency if the pass the soundness
> check. Nonsense definitions can lead to results that a mathematician might
> consider nonsense, but you can't prove a contradiction assuming ZFC is
> consistent. We could swap the definitions of 4 and 5 (i.e. swap those
> symbols throughout set.mm) and have some strange looking results like
> 2+2=5, but although that violates the human convention for those symbols,
> we still can't prove a contradiction.
>
> Norm
>
--
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/84daecf7-502b-41e8-8a41-2c942f4066ca%40googlegroups.com.
