What is the first order axiom characterizing a field having characteristic zero?

Question

In this thread on the axioms of $\mathbb Q$ it's stated that a field having characteristic zero can be written down in first-order logic. The definition in the logic lecture notes I work with (by Stephen G. Simpson) give the standard definition, which isn't a formal first order statement:

$$"(1+1+\ \dots\ +1+1)_{n\ \text{times}}\neq0"$$

Now in this Wikipedia page on periodic groups (and in the reference given there, I looked it up), it is stated that a group being periodic

$$"\forall x.\, ((x=e) \lor (x\circ x=e) \lor ((x\circ x)\circ x=e) \lor \ldots)"$$

can't be stated in first-order logic. Both would be "for all $n\in \mathbb N$" statements and it makes my question how the characteristic zero axiom can be a first-order statement and secondly if we can formally pull off $\mathbb Q$ without first formalize $\mathbb N$.

My question is: What is the first order axiom characterizing a field having characteristic zero?

Answer 1

There is no single axiom doing that. But rather a schema of axioms stating that the characteristic is not positive of any possible value.

To see that this is the case, consider the ultraproduct of all prime fields of finite order, with a free ultrafilter. The result is a characteristics $0$ field. And any statement true in that field is true in infinitely many finite fields. So there cannot be a single axiom stating that the characteristics is $0$.

Answer 2

What one means by declaring $$(1+1+\cdots+1+1)_{n\text{ times}}\neq0$$ to be an axiom (schema!) is that each of the formulas $$ \begin{align} 1 &\neq 0 \\ 1+1 &\neq 0 \\ 1+1+1 &\neq 0 \\ 1+1+1+1 &\neq 0 \end{align} $$ and so forth, is separtely an axiom.

As Asaf argues, the resulting theory of fields of characteristic 0 is not finitely axiomatizable, but there is nothing intrinsically wrong with having a theory with infinitely many axioms, as long as there's a definite way to determine whether a given formula is an axiom or not.

Axiom schemas are also used in the usual first-order theories for basic arithmetic (Peano Arithmetic with its induction axiom schema) or set theory (ZFC with axiom schemas for selection and replacement).

Answer 3

The problem with the group theory case is that there is no natural way to break up an infinite $\lor$ into separate axioms. But the infinite axiom scheme for $\mathbb Q$ is representing an infinite $\land$, so we can break it up into separate axioms.