Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Definition of complex number apartness looks too strong #4131

Open
benjub opened this issue Aug 15, 2024 · 1 comment
Open

Definition of complex number apartness looks too strong #4131

benjub opened this issue Aug 15, 2024 · 1 comment

Comments

@benjub
Copy link
Contributor

benjub commented Aug 15, 2024

...though it turns out to be correct !

Indeed, the current definition https://us.metamath.org/ileuni/df-ap.html defines two complex numbers as being apart from each other if their real parts are apart or their imaginary parts are apart. This is the intuitionistic "or", which is "strong": this implies that if two complex numbers are apart, you can prove that their real parts are apart or you can prove that their imaginary parts are apart.

A more cautious definition seems to be in terms of their distance being (strictly) positive. Depending on how you express that distance at that point of the development, something like

$z\not\neq w \leftrightarrow 0 < (z-w)^* (z-w)$

Then, this implies the current definition, because $\mathbb{C}$ is finite-dimensional as an $\mathbb{R}$-vector space: if $0 < a < (z-w)^* (z-w)$ then you can prove $a/4 < (\Re(z-w))^2 \vee a/4 < (\Im(z-w))^2$, etc. But formalizing that in iset.mm looks like it would involve sizeable changes since for instance theorems about the archimedean property use tightness of real apartness ~ax-pre-apti, so there would be some re-ordering of theorems.

(To a lesser extent, this applies to real apartness itself: define $x \not\neq y$ as $0<(x-y)^2$, and from $0<(x-y)^2$ you deduce $x < y \vee y < x$... but here, it would probably become almost tautological, since we will use ~ax-pre-apti.)

Still, it is the practice in (i)set.mm to have the "official" definition df-xxx be minimal, and then prove "alternate definitions" dfxxx2, etc., suited to later applications

Any thoughts ? (FYI @jkingdon @digama0)

@jkingdon
Copy link
Contributor

jkingdon commented Aug 15, 2024

I'm more concerned with showing equivalences (as we do with many dfxxxxn type theorems) than I am in worrying too much about which one is the $a and which one is the $p derived from it.

The df-ap we have now is taken directly from the cited source, and at least so far seems to have all the expected properties (irreflexivity, symmetry, cotransitivity, tightness, interaction with addition, multiplication, recirpocal, etc).

Adding some equivalences of the form x =//= y <-> .... seems like a good next step to me. It also means having the chance to work out various alternatives, ensure they really are equivalent, etc, before getting into the harder work of digging deeply into what we define in what order and what depends on what (which we can still do later if we want, I'm mostly saying don't start with that part).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants