Formal systems need not be consistent; if a formal system assumes both P and ~P as axioms, you can derive S and ~S (for any S) by explosion.

Is the problem that you can't proof consistency? Because if it's consistent then shouldn't either P or ~P be true or the axiom doesn't exist?

It is possible to prove consistency but to do so requires using a more powerful system of axioms which in turn might be inconsistent. What Goedel showed is that in any system that can encode arithmetic (and consequently some notion of computation, e.g. lambda calculus) can not be complete if it is consistent.

Ah, thank you, that makes more sense. Maybe a weird follow-up question: Is it possible (or does it make sense) to find a proof in an inconsistent system and to try to "transform" it into a consistent one?

Yes, paraconsistent logic could be considered an instance of such a system: https://en.wikipedia.org/wiki/Paraconsistent_logic.