structures*. 5. Thus EVEN on finite ordered structures cannot be expressed in FO. (*) Note that the proof of the result of the Ehrenfeucht–Fraïssé game has been omitted, since it is not the main focus here. Zero-one laws and, independently, proved a zero–one law for first-order sentences in finite models; Fagin's proof used the compactness theorem. According to this result, every first-order sentence in a relational signature is either almost always true or almost always false in finite -structures. That is, let be a fixed first-order sentence, and choose a random -structure with domain , uniformly among all -structures with domain . Then in the limit as tends to infinity, the probability that models will tend either to zero or to one: The problem of determining whether a given sentence has probability tending to zero or to one is PSPACE-complete. A similar analysis has been performed for more expressive logics than first-order logic. The 0-1 law has been shown to hold for sentences in FO(LFP), first-order logic augmented with a least fixed point operator, and more generally for sentences in the infinitary logic , which allows for potentially arbitrarily long conjunctions and disjunctions. Another important variant is the unlabelled 0-1 law, where instead of considering the fraction of structures with domain , one considers the fraction of isomorphism classes of structures with elements. This fraction is well-defined, since any two isomorphic structures satisfy the same sentences. The unlabelled 0-1 law also holds for and therefore in particular for FO(LFP) and first-order logic. Descriptive complexity theory An important goal of finite model theory is the characterisation of complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity classes in the polynomial hierarchy, is precisely the class of languages expressible by statements of second-order logic. This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them. Specifically, each logical system produces a set of queries expressible in it. The queries – when restricted to finite structures – correspond to the computational problems of traditional complexity theory. Some well-known complexity classes are captured by logical languages as follows: In the presence of