N satisfying the universal axioms of ACFp is a substructure of a sufficiently large algebraically closed field , and additionally any two such embeddings N → M induce an automorphism of M. Finite fields The theory of finite fields is the set of all first-order statements that are true in all finite fields. Significant examples of such statements can, for example, be given by applying the Chevalley–Warning theorem, over the prime fields. The name is a little misleading as the theory has plenty of infinite models. Ax proved that the theory is decidable. Formally real fields The axioms for fields plus, for every positive integer n, the axiom: ∀ a1 ∀ a2... ∀ an a1a1+a2a2+ ...+anan=0 → a1=0∧a2=0∧ ... ∧an=0. That is, 0 is not a non-trivial sum of squares. Real closed fields The axioms for formally real fields plus the axioms: ∀x ∃y (x=yy ∨ x+yy= 0); for every odd positive integer n, the axiom stating that every polynomial of degree n has a root. The theory of real closed fields is effective and complete and therefore decidable (the Tarski–Seidenberg theorem). The addition of further function symbols (e.g., the exponential function, the sine function) may change decidability. p-adic fields showed that the theory of p-adic fields is decidable and gave a set of axioms for it. Geometry Axioms for various systems of geometry usually use a typed language, with the different types corresponding to different geometric objects such as points, lines, circles, planes, and so on. The signature will often consist of binary incidence relations between objects of different types; for example, the relation that a point lies on a line. The signature may have more complicated relations; for example ordered geometry might have a ternary "betweenness" relation for 3 points, which says whether one lies between two others, or a "congruence" relation between 2 pairs of points. Some examples of axiomatized systems of geometry include ordered geometry, absolute geometry, affine geometry, Euclidean geometry, projective geometry, and hyperbolic geometry. For each of these geometries there are many different and inequivalent systems of axioms for various dimensions. Some of these axiom systems include "completeness" axioms that are not first order. As a typical example, the axioms for projective geometry use 2 types, points and lines, and a binary incidence relation between points and lines. If point and line variables are indicated by small and capital letter, and a incident to