Why is this definition of complex numbers "informal"? 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.
 A: 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)$.
A: You can't just let a deus ex machina do all your work and deliver you an object with properties you want. You can wonder what happens if such an object exists, but to justify your thoughts you have to create a model where this object is defined and happens to have the desired properties. 
In this particular case, if you work with some of the models given above it turns out they all result in the same (up to renaming the elements) field $C$ (fulfilling all the field properties!) which contains the reals (in particular it contains $-1\in R$) and in which there exists some number $i$ satisfying $i^2=-1$ and in which furthermore every number can be written as $a+bi$, $a,b\in R$. Once you know such models exists your thoughts from before are justified.
A: I think the answer by Denis correctly identifies what is "informal" about the first definition.
I also think that the first definition would perhaps be better labeled the "historical" definition, as it seems to be the manner in which complex numbers came into use in the first place. If you look at some of the old texts explaining the solution of the cubic equation, for example, you can find the notation $rm1$ (or something very like it; this is from memory), where evidently $m$ indicates a negative number ("minus") and $r$ indicates taking the square root. In other words, people started working with complex numbers by introducing the new quantity $\sqrt{-1}$ into their formulas.
To summarize some of the other discussion, you could in fact make a formal definition that introduced a new object $i$ with the necessary axioms ($i^2 = -1$, I'm not sure what else), but you can make a model of $\mathbb{C}$ using nothing more than the same set-theoretic axioms and definitions from which we can construct $\mathbb{R}$, so why would you want to introduce a new axiom?
Back to the historical viewpoint, at the time $\mathbb{C}$ was first invented the ZFC definition of $\mathbb{R}$ was still unknown, so using it to model $\mathbb{C}$ was not an option. But that was then, and this is now.
