> 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.
I know this. The paragraph you're referring to was about the formalization
in Lean. 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".
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.
>
As I wrote in my first post, I took df-iota as an example for the sake of
concreteness. My goal is mainly exploratory, and not restricted to set.mm:
see the different things that can be done regarding undefined terms, with
their pros and cons. I already learnt a few things from Mario's answer,
maybe some other readers did too, and it's already good enough for me.
Benoît
> 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 ?
>>>
>>
>> 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/831918ac-a860-409b-b281-1d555d8bc8f8%40googlegroups.com.
