Suppose that a first-order formula described the inaccessible cardinal , so that were the least ordinal with . Since is inaccessible, is a model of ZFC. Apply the Lévy reflection theorem inside this model to the single formula . There is some for which
The right side holds, so the left side contradicts the asserted minimality of . Hence no first-order formula describes an inaccessible cardinal, as recorded by ordinal described by a first-order formula.
The compactness theorem says that a set of first-order sentences has a model if and only if every finite subset of has a model. One implication follows by taking the same model. Conversely, if had no model, then by the Godel completeness theorem it would prove a contradiction. A formal proof uses only finitely many assumptions, so some finite subset of would already have no model. This contradiction proves compactness.
The Upward Lowenheim-Skolem theorem says that if an -theory has an infinite model, then it has models of arbitrarily large cardinality; more precisely, it has a model of cardinality at least for every cardinal . Add new constants for and the sentences
Every finite subset of the enlarged theory can be interpreted in the given infinite model, since it mentions only finitely many constants. Compactness supplies a model of the whole enlarged theory, in which the are pairwise distinct. Its reduct to is a model of having at least elements. If , the Downward Lowenheim-Skolem theorem gives a model of cardinality exactly .
Since the strongly inaccessible cardinal is inaccessible, is a model of ZFC. The Downward Lowenheim-Skolem theorem gives an elementary substructure
of cardinality such that
One may obtain concretely as the Skolem hull of this set; its cardinality remains because the language of set theory is countable and .
Apply the Mostowski collapse theorem to and write for the collapse. Then is a transitive set, , and fixes pointwise. It also fixes , because it fixes every ordinal below . By elementarity, satisfies ZFC and regards as a kappa-complete filter that is a nonprincipal ultrafilter on . Therefore, with ,
The internal ultrafilter need not equal the original .