It suffices to obtain a model of ZFC without weakly inaccessible cardinals. Starting with any model of ZFC, pass to its constructible universe, which satisfies ZFC and the Generalized continuum hypothesis. If it has no inaccessible cardinal, use that model. Otherwise pass to its rank segment at its least inaccessible cardinal . This segment satisfies ZFC, retains the Generalized continuum hypothesis, and has no inaccessible cardinals. Under the Generalized continuum hypothesis, every weakly inaccessible cardinal is strongly inaccessible: if and is a limit cardinal, then . Thus in either case the resulting model has no weakly inaccessible cardinals.
Work inside . If is a nonzero limit ordinal, let . It is an uncountable limit cardinal. If it were regular, it would be a weakly inaccessible cardinal, which is impossible in . It is therefore singular, and the singular cardinal enumeration is continuous at this index:
The cofinality of an increasing ordinal supremum now gives
for every nonzero limit ordinal in . Hence satisfies the negation of the proposed existential assertion. By the soundness theorem for first-order logic, consistency of ZFC prevents ZFC from proving that assertion. The model construction is a relative-consistency argument; it does not assume that consistency alone supplies a countable transitive model. Here, as usual, a limit ordinal excludes zero.
Let be ZFC together with the assertion of unboundedly many inaccessible cardinals. Given a model of , if it has no inaccessible limit of inaccessibles, it already witnesses the required nonimplication. Otherwise let be its least inaccessible limit of inaccessibles and pass to its rank segment .
Because is an inaccessible cardinal, satisfies ZFC. Its ordinals are precisely those below , and below the inaccessible cardinals are unbounded by the choice of . Inaccessibility of any smaller ordinal is absolute to this segment: it has the same subsets and functions on all smaller ordinals, as in strong-inaccessibility absoluteness from rank agreement. Thus satisfies the unbounded-inaccessibles assertion.
No smaller ordinal can be an inaccessible limit of inaccessibles, by minimality of and the same absoluteness. Also is not an ordinal of itself. Consequently
This rank cutoff at the first inaccessible limit of inaccessibles proves . The soundness theorem for first-order logic then gives if is consistent. This is a model-theoretic relative-consistency argument, and does not infer external transitivity from mere consistency.
The Godel completeness theorem says that for every first-order theory and sentence ,
Together with soundness, this is equivalence; it is also equivalent to saying that every syntactically consistent first-order theory has a model.
The compactness theorem states that a set of first-order sentences has a model if and only if every finite subset has a model. To deduce it, suppose every finite subset is satisfiable but is not. Then , so completeness gives a formal proof . A proof uses only finitely many assumptions, yielding some finite , contrary to that subset's satisfiability.
Suppose first that . By the soundness theorem for first-order logic, every theorem of is true in . A contradiction cannot be true in a structure, so is consistent.
Conversely, the Godel completeness theorem says that every semantically valid consequence is derivable. Its equivalent model-existence form says directly that every consistent first-order theory has a model. Hence