Axiomatization of field theory for the Knuth-Bendix algorithm?

Question

Is there an axiomatization of Field Theory suitable for the Knuth-Bendix algorithm? If not, would the creation of such an axiomatization be of publishable academic interest?

Answer 1

In the comments, you clarify that by an axiomatization of field theory suitable for the Knuth-Bendix algorithm, you mean a set of first-order sentences, each of which is a (universally quantified) equation between terms.

Such an axiomatization / theory is usually called an equational axiomatization or equational theory. Equational theories, or rather their classes of models (such a class is called a variety of algebras) are the main objects of study in universal algebra.

It is well-known that the class of fields does not admit an equational axiomatization. Why? Any variety of algebras is closed under substructures, products, and homomorphic images (i.e. quotients by congruences). In fact, the HSP theorem says that a class of structues (in a language with constants and function symbols, no relation symbols) is a variety of algebras if and only if it is closed under substructures, products, and homomorphic images.

Fields (as structures in the language $\{+,-,\times,0,1\}$) fail to be closed under all three of these operations:

• $\mathbb{Z}$ is a substructure of $\mathbb{Q}$, but it is a not a field.
• The product $\mathbb{Q}\times \mathbb{Q}$ is not a field.
• The zero ring $\{0\}$ is a homomorphic image of $\mathbb{Q}$ (by the map sending every element of $\mathbb{Q}$ to $0$), but it is not a field.

You might hope to give an equational axiomatization of fields in a different language. For example, if you add a symbol $^{-1}$ for multiplicative inverse and decide by convention that $0^{-1} = 0$, then any substructure of a field is a field. But in this language, fields still fail to be closed under products and homomorphic images. The smallest variety of algebras containing the fields in this language is called the class of meadows.

In fact, the goal of giving an equational axiomatization of the class of fields, even in some non-standard language, is doomed to fail. The reason is that any variety of algebras contains the one-point algebra in which all terms are equal (and hence all axioms are satisfied). But there is no field with one element (well, except in a quite different very non-literal sense).