A is written as aA, then one set of axioms is (There is a line through any 2 distinct points a,b ...) (... which is unique) (Veblen's axiom: if ab and cd lie on intersecting lines, then so do ac and bd.) (Every line has at least 3 points) Euclid did not state all the axioms for Euclidean geometry explicitly, and the first complete list was given by Hilbert in Hilbert's axioms. This is not a first order axiomatization as one of Hilbert's axioms is a second order completeness axiom. Tarski's axioms are a first order axiomatization of Euclidean geometry. Tarski showed this axiom system is complete and decidable by relating it to the complete and decidable theory of real closed fields. Differential algebra The theory DF of differential fields. The signature is that of fields (0, 1, +, −, ×) together with a unary function ∂, the derivation. The axioms are those for fields together with For this theory one can add the condition that the characteristic is p, a prime or zero, to get the theory DFp of differential fields of characteristic p (and similarly with the other theories below). If K is a differential field then the field of constants The theory of differentially perfect fields is the theory of differential fields together with the condition that the field of constants is perfect; in other words, for each prime p it has the axiom: (There is little point in demanding that the whole field should be a perfect field, because in non-zero characteristic this implies the differential is 0.) For technical reasons to do with quantifier elimination, it is sometimes more convenient to force the constant field to be perfect by adding a new symbol r to the signature with the axioms The theory of differentially closed fields (DCF) is the theory of differentially perfect fields with axioms saying that if f and g are differential polynomials and the separant of f is nonzero and g≠0 and f has order greater than that of g, then there is some x in the field with f(x)=0 and g(x)≠0. Addition The theory of the natural numbers with a successor function has signature consisting of a constant 0 and a unary function S ("successor": S(x) is interpreted as x+1), and has axioms: ∀x ¬ Sx = 0 ∀x∀y Sx = Sy → x = y Let P(x) be a first-order