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/8a17a9ed-9d8f-4632-893d-df56bc18c780%40googlegroups.com.
