Non-contradictory axiom system for a binary operation

Question

Suppose we want to define a binary operation $\otimes:\mathbb{N} \times\mathbb{N} \rightarrow \mathbb{N}$ on a ring $(\mathbb{N},+,\cdot)$ with an arbitrary system of axioms. The axioms may be given both using only "$\otimes$" itself (e.g. "$a\otimes b = b \otimes a$") or also the already existing ring structure (e.g., "$a\otimes b = 100\cdot a + b$"). Is there a methodical way to check whether this system is self-contradictory?

Answer 1

No. For example, we could write down the axioms (1) $a\otimes a= 1$ if $a$ is a counterexample to Goldbach's conjecture, and (2) $a\otimes a=0$ for all $a$. These axioms are consistent if and only if Goldbach's conjecture is true. Since Goldbach's conjecture has been open for hundreds of years, I hope this convinces you that there is no methodical way to check consistency.

For a more technical answer, we could write down axioms asserting (1) $a\otimes b=0$ if the Turing machine $a$ halts on input $b$ and $a\otimes b=1$ otherwise, and (2) $n\otimes m=0$ for a fixed $n$ and $m$. Now an algorithm to check consistency of (1) and (2) would amount to a solution to the halting problem, and it is a theorem that no such algorithm exists.

p.s. $(\mathbb{N},+,\cdot)$ is not a ring, it's a semiring.