I'm reading the proofwiki page about complex number: https://proofwiki.org/wiki/Definition:Complex_Number
According to proofwiki there is an informal and formal definitions of complex numbers. The informal definition is that a complex number is equal to $a+bi$ where $a,b \in \Bbb R$ and where $i$ is defined to be the square root of $-1$. What is informal about this definition ?
I guess that this is because you can just define $i$ to be so that $i^2=-1$. But I don't totally get why this is. Would it be formal if I defined $i$ as a number that has all field properties of real numbers, and $i^2=-1$ ?
The only problem I see is that you could argue that there are 2 of those numbers. So which one is meant ? But if you prove that it doesn't matter which one you pick, would this definition then be formal ?
Btw, I'm aware that my reasoning is probably wrong, but I think it is helpfull if I share what is going on in my mind.
This definition is "informal" because the square root was defined to be a function $\mathbb R^+ \to \mathbb R$, and $\sqrt{-1}$ makes no sense in terms of this previous definition.
Indeed, the formal way is close to what you say. But we don't want to create a number $i$ out of thin air, and postulate properties about it. Ideally we want to define it in terms of objects we know, using standard mathematical constructions. To do it completely formally within set theory, a way to define complex numbers is by pairs $(a,b)\in \mathbb R^2$, and define addition $(a,b)+(a',b')=(a+a',b+b')$ and multiplication $(a,b)\times(a',b')=(aa'-bb',ab'+ba')$. Then $i$ is just a shortcut notation for $(0,1)$, and when we write $a+ib$ we really mean $(a,b)$.