An omega-saturated model realizes every complete type of a finite tuple over every finite set of its domain. It suffices to require this for one-variable types: realize the coordinates successively, enlarging the finite parameter set at each step.

Every complete theory here has such a model, with no countability requirement on its size. Start with a model of size at most $\lambda =2^{{\aleph }_0}$. There are at most $\lambda$ types over its finite sets, because the language is countable and each such type is a set of formulas in a countable collection. By the compactness theorem and the elementary diagram construction, pass to an elementary extension realizing all these types, keeping size at most $\lambda$ by the Löwenheim-Skolem theorem.

Repeat this for stages $0,1,2,\dots$ and take the union of the elementary chain. Any finite parameter set in the union lies in some stage, and every type over it is realized at the next stage. The union is therefore omega-saturated. Countable language does not by itself guarantee that a countable saturated model exists.

The countable omitting types theorem says that for a consistent theory in a countable language and countably many nonprincipal types of finite arities, there is a countable model omitting all those types. In particular a nonisolated complete type of $T$ can be omitted in a countable model.

Interpret “definable” here as without parameters. If parameters were allowed freely, every infinite structure would have infinitely many definable singleton sets, and the claimed implication would be false even for a dense linear order without endpoints.

Infinitely many distinct parameter-free definable subsets of $A^n$ imply infinitely many complete $n$-types: if there were only $r$ such types, each formula would select a subset of those $r$ types, giving at most $2^r$ distinct definable subsets. There must also be a nonisolated complete type. To see this, suppose each complete type $p$ had an isolator ${\theta }_p$. The family of their basic open sets covers the type space. Its compactness theorem gives a finite subcover, which would account for only finitely many complete types, a contradiction. Equivalently apply logical compactness theorem to $T\cup \{\neg {\theta }_p(c):p\text{ complete}\}$.

Choose a nonisolated type $p$. The omitting types theorem gives a countable model omitting it, while part (d) gives a countable model realizing it. An isomorphism of structures preserves realization of parameter-free types, so these models are not isomorphic. Thus $\boxed{T\text{ is not }{\aleph }_0\text{-categorical}}$.

Add constants $c_1,\dots ,c_n$ and form $T\cup \{\phi (c):\phi \in p\}$. Every finite set has a model by consistency of the type. The compactness theorem gives a model $\mathcal{M}$ realizing the whole expanded theory, so $c^{\mathcal{M}}$ realizes $p$.

Apply the downward Löwenheim-Skolem theorem to the countable expanded language, retaining these finitely many named elements. The resulting countable elementary substructure still satisfies every formula of $p$ at the same tuple. Its reduct to the original language is a countable model of $T$ realizing $p$. Since $T$ has no finite models, this model is countably infinite.

Let $\theta (x)$ isolate the principal type. Consistency with $T$ means $T\cup \{\exists x\theta (x)\}$ is satisfiable. Because $T$ is a complete theory, it must imply $\exists x\theta (x)$; the alternative would make that extension inconsistent.

Therefore every model of $T$ has a tuple $a$ satisfying $\theta$. Each implication $T\models \theta \to \phi$ then makes $a$ satisfy every member of the type. HenceCompleteness is what turns possible realization of the isolating formula into realization in every model.

An $n$-type over the empty set is a set $p(x_1,\dots ,x_n)$ of formulas of the language, with no additional parameters, jointly consistent with $T$. Equivalently every finite set is simultaneously satisfiable with $T$. A complete type decides every formula in these variables: for each $\phi$, exactly one of $\phi$ and $\neg \phi$ belongs to $p$.

A principal type has an isolating formula $\theta (x)$ consistent with $T$, such that $T\models \forall x(\theta (x)\to \phi (x))$ for every $\phi \in p$. For a complete type this is an isolated type; its isolator determines the entire type. A principal partial type may be weaker than a complete type, so its isolator need not decide all formulas.

A tuple $a\in A^n$ realizes $p$ if $\mathcal{A}\models \phi (a)$ for every formula in $p$. The model omits $p$ if it contains no such tuple. Thus omission is a simultaneous failure of realizing the whole type, even though each finite fragment can be realized.

A complete theory is $\kappa$-categorical when it has a model with underlying cardinality $\kappa$ and any two of its models of that cardinality are isomorphic structures. Thus categoricity means uniqueness up to isomorphism at the specified cardinal, not a unique underlying set or a unique isomorphism.

For the infinite cardinals relevant here, the existence clause is automatic from the stated infinite model and the Löwenheim-Skolem theorem. One may equivalently require exactly one isomorphism class of models of size $\kappa$.

One can takeFor the first formula, the Löb axiom with conclusion $\perp$ gives $\square (\square \perp \to \perp )\to \square \perp$, that is, $\square F_1\to \square \perp$. Conversely, the tautology $\perp \to F_1$, necessitation rule, and distribution give $\square \perp \to \square F_1$. Thus $GL⊢\square F_1\leftrightarrow \square \perp$. Negating both sides gives $GL⊢\neg \square F_1\leftrightarrow F_1$.

For the second formula, $\neg F_2=\top$ is a theorem, so $GL⊢\square \neg F_2$. Hence $\neg \square F_2\wedge \neg \square \neg F_2$ is false in the logic and is equivalent to $\perp =F_2$. A fixed point is a formula satisfying the equivalence; it need not itself express a nontrivial undecidable assertion.

Take the outermost boxed subformulas of $X(p)$ containing the distinguished letter. Because $X$ is modalized in $p$, every occurrence of $p$ lies inside one of these boxes. The supplied decomposition therefore has the formwhere $H$ has no occurrence of $p$. Other letters and subformulas not involving $p$ may be retained as parameters in $H$ and the $C_i$.

Introduce temporary letters $q_1,\dots ,q_m$ and solve the boxed systemby part (b), obtaining $Q_i$ without the temporary letters or $p$. Put $F=H(Q_1,\dots ,Q_m)$. Each solved equation gives $GL⊢Q_i\leftrightarrow \square C_i(F)$. The supplied replacement-of-equivalents principle then givesOnly letters already present in $X$, apart from the removed $p$, occur in the constructed $F$. If $p$ is absent from $X$ to begin with, take $F=X$. This is the modalized fixed-point theorem for GL, proved by finite elimination rather than a semantic completeness argument.

The language of Gödel-Löb logic has propositional variables, $\perp$, implication, and the unary operator $\square$; the other logical connectives are abbreviations. Its axioms are all classical tautologies, the distribution scheme $\square (A\to B)\to (\square A\to \square B)$, and the Löb scheme $\square (\square A\to A)\to \square A$. Its rules are modus ponens rule, necessitation rule of theorems, and uniform substitution.

For a single boxed equation $p\leftrightarrow \square C(p)$, set $F=\square C(\top )$. The identity supplied in the source gives directly $GL⊢F\leftrightarrow \square C(F)$. If $p$ does not occur, take $F=\square C$ instead.

Proceed by induction for a system of $m$ equations, allowing other propositional variables as parameters. Treat $p_1,\dots ,p_{m-1}$ as parameters in the last equation and putThe one-variable result proves $D\leftrightarrow \square C_m(p_1,\dots ,p_{m-1},D)$. Substitute this $D$ for $p_m$ in the first $m-1$ equations. They are still boxed equations, so induction supplies solutions $F_1,\dots ,F_{m-1}$. Define $F_m=D(F_1,\dots ,F_{m-1})$.

By construction, the first $m-1$ equations hold after this substitution; substituting into the theorem for $D$ proves the last. HenceThe elimination introduces no new parameter letters and removes every unknown letter. This gives a constructive simultaneous boxed fixed-point elimination in GL.

Abbreviate the arithmetical provability predicate by $\square$, with the Hilbert-Bernays-Löb derivability conditions understood. Löb's theorem saysChoose a diagonal sentence $D$ with $S⊢D\leftrightarrow (\square D\to A)$. Internalizing its forward implication gives $S⊢\square D\to \square (\square D\to A)$. Internal modus ponens rule gives $\square (\square D\to A)\to (\square \square D\to \square A)$, while positive introspection gives $\square D\to \square \square D$. Combining these yields $S⊢\square D\to \square A$.

Now use the assumed theorem $\square A\to A$. It follows that $S⊢\square D\to A$, and the reverse direction of the diagonal equivalence gives $S⊢D$. External necessitation rule gives $S⊢\square D$, and the previously derived implication gives $S⊢A$. This proves the theorem from the supplied fixed-point property and the derivability conditions.

The Gödel second incompleteness theorem states that a consistent arithmetic theory in this setting cannot prove its own consistency sentence ${\mathrm{Con}}_S=\neg \square \perp$. If it could, it would prove $\square \perp \to \perp$; applying Löb's theorem with $A=\perp$ would make it inconsistent. Therefore $\boxed{S⊬{\mathrm{Con}}_S}$ when $S$ is consistent.