I was studying calculus and while reading the axioms of a field I was trying to write them all only using logic notation. Although, I’m not quite confident if the following statement
$$\forall x \in \mathbb{K} \, , \, \exists y,z \in \mathbb{K} \, \colon \; [\, ( \neg [\, \forall w \in \mathbb{K} \, , \; x + w = w \,] \implies x \cdot y = z ) \, \wedge \, ( \forall a \in \mathbb{K} \, , \; [\, \neg (\forall b \in \mathbb{K} \, , \; z + b = b ) \, \wedge \, ( \neg [\, \forall c \in \mathbb{K} \, , \; a + c = c \,] \implies z \cdot a = a ) \,] ) \,]$$
correctly states the existence of a inverse element for every non-zero element. Can you give me some feedback? Thank you for your attention!
Note. I wish to avoid the use of symbol $0$ for the identity for addition.
In the first-order form of fields, we say that for ($\mathbf{F}$, +, $\cdot$, $0$ , $1$) where $0 \neq 1$, that the inverse axiom under multiplication is $$\forall x \; \exists y \; (y \cdot x = 1 \; \leftrightarrow \; x \neq 0)$$ Under addition $$\forall x \; \exists y \; (x + y = 0)$$ You don't need to prove the statements as they're axioms, because it seems like you're going for a proof there. If you don't want to put the $0$ like you said in the comments, then say $$\forall x \;\exists y \; (y \cdot x = 1 \; \leftrightarrow \; \forall z \; (z + x \neq z))$$
I hope this answers your question. :)
Edit:
I'm going to critique your formalization too as requested at the end. First, I'm going to put it into Prenex so it is easily read:
$$\forall x \; \exists z \; \Bigg(\Big(\forall w \;\lnot (x + w = w) \to \exists y \; (x \cdot y = z)\Big) \; \land \; \big(\forall b \; \lnot (z + b = b)\big) \; \land \; \bigg(\forall a \Big(\; \forall c \; \lnot (a + c = c) \; \to \; (z \cdot a = a)\Big)\bigg) \Bigg)$$ Now, this is saying that if not all elements are identity elements then there is an identity element $z$, and it is not an additive element, and also that it is the multiplicative identity. Now, I see this as redundant as the symbol $z$ here acts like the symbol $1$ (replace every $z$ with $1$, and you'll see what I mean) so, you've reached the same conclusion, and it won't be exactly the same as $z$ is not constant now but merely has the same properties. A constant is different from a variable in first-order logic, and so it is stated without a quantifier. Also that, even if we would ignore all of the listed problems, assume that the left-hand side of each implication is false, then the implication is still true, and therefore it could be an identity element at the same time (if not for the middle-clause between the conjunction). I suggest putting it like this (to ensure they're both distinct) $$\forall x \; \exists y \; \exists b \; \big((x + y = x) \; \land \; \forall a \; (a \cdot b = a) \; \leftrightarrow \; y \neq b \big)$$ If not wanted, then remove the left-hand side of each implication (and the implication itself while leaving the right side), and it would say the same thing. I.e. $$\forall x \; \exists z \; (\exists y \; (x \cdot y = z) \; \land \; (x + z \neq x) \; \land \; (x \cdot z = x))$$