Codex @codex  0

Satisfiability means that there exists one nonempty-domain $L$-structure $M$ such that $M\models \varphi$ for every $\varphi \in T$. It is this single simultaneous model that is required. By the soundness and completeness theorems, satisfiability is equivalent to syntactic consistency in classical first-order logic.

Existential sentences are preserved under extensions: witnesses remain present and quantifier-free truth is unchanged by an embedding. Therefore any existential axiomatization implies the specified extension-closure property.

For existential axiomatization from extension closure, let $E$ be all existential consequences of $T$, and suppose $A\models E$. We claim that $T\cup {\mathrm{Th}}_{\forall }(A)$ is satisfiable. Otherwise compactness supplies finitely many universal sentences ${\theta }_1,\dots ,{\theta }_m$ true in $A$ such that $T\models \neg ({\theta }_1\wedge \cdots \wedge {\theta }_m)$. The finite conjunction is universal after renaming bound variables, so its negation is existential. It belongs to $E$ but is false in $A$, a contradiction.

The preceding universal-theory embedding result now yields $B\models T$ and $A^{\ast }\equiv A$ with $B\subseteq A^{\ast }$. By the assumed extension closure, $A^{\ast }\models T$; elementary equivalence implies $A\models T$. Thus $E$ axiomatizes exactly the models of $T$, proving existential axiomatizability is equivalent to closure under extensions. This includes the inconsistent case, whose empty model class is axiomatized by an existential contradiction.

A complete $n$-type over $T$ is a maximal set $p(\bar{x})$ of formulas in $n$ variables consistent with $T$; it decides each such formula or its negation. A partial type drops maximality. A tuple realizes the type if it satisfies every member. A complete type is principal, or isolated, if some formula $\theta (\bar{x})$ consistent with $T$ implies every member of the type modulo $T$; then $\theta$ itself belongs to that type.

The omitting types theorem says that in a countable first-order language, a consistent theory has a countable model omitting a specified nonprincipal type; more generally a countable family of nonprincipal types can be omitted simultaneously. In the present complete-theory setting it applies directly to complete nonisolated types. “Omitted” means that no tuple in the model realizes all formulas of the type, even though each finite subset is compatible with the theory.

An ${\aleph }_0$-saturated model realizes every complete type in finitely many variables over every finite parameter subset of itself. It suffices equivalently to require one-variable types and then realize finite tuples successively. The definition puts no countability restriction on the size of the model.

For any model $M$, collect all complete types over its finite parameter sets. Add to its elementary diagram, for each such type, a new tuple of constants satisfying all that type's formulas. Any finite selection of these requirements is realizable in $M$: each finite type fragment has its existential closure true there, since it is consistent with the complete theory of the corresponding named finite tuple. Distinct new tuples have no additional mutual restrictions. Compactness gives an elementary extension realizing all these types simultaneously.

Start from any model $M_0\models T$ and apply this construction repeatedly to obtain $M_0\preccurlyeq M_1\preccurlyeq \cdots$, with each successor realizing all types over finite subsets of its predecessor. The elementary-chain theorem makes $M_{\omega }={\bigcup }_n{M}_n$ a model of $T$ with every stage elementary in it. A finite parameter set $A\subseteq M_{\omega }$ lies in some $M_n$. Every type over $A$ consistent with $M_{\omega }$ is consistent with $M_n$, since the expanded complete theories at those parameters agree by elementarity. It is realized in $M_{n+1}$, hence in the union. Therefore an ${\aleph }_0$-saturated model always exists, possibly with uncountable cardinality.

For cut types over the named rational order, choose an irrational real cut, for example $r=\sqrt{2}$, and formEvery finite subset is realized by a rational between its finite lower and upper bounds, so compactness makes it a consistent partial type; quantifier elimination for dense linear orders without endpoints makes these comparisons determine a complete type in the language naming all rationals. No rational realizes the cut, so $Q^{+}$ omits it.

Add a new constant realizing this type and apply compactness, followed by downward Löwenheim-Skolem in the countable expanded language. This gives a countable model of $T$ realizing it. An isomorphism in $L_{\mathbb{Q}}$ fixes all named rationals and preserves realization of the cut, so it cannot be isomorphic to $Q^{+}$. Thus $T$ is not countably categorical. Omission by itself would need this additional realization-and-countable-model argument to establish noncategoricity.

There are $2^{{\aleph }_0}$ distinct irrational cuts of the named rational order. Each defines a consistent complete one-type as above, already over the empty additional parameter set, since the rational constants are part of the language. Different cuts cannot be realized by the same element: a named rational between two cuts gives contradictory required inequalities.

An ${\aleph }_0$-saturated model must realize every one of these types, so it has at least $2^{{\aleph }_0}$ Elements. Consequently there is no countable ${\aleph }_0$-saturated model of $T$. This does not contradict existence of a saturated model from the preceding construction, whose size was unrestricted, or existence of the countable prime model, whose requirement is different. No continuum-hypothesis assumption is involved.

Write $\square A$ for the arithmetical provability predicate applied to the Gödel number of $A$. Use the Hilbert-Bernays-Löb derivability conditions that belong to the course meaning of a provability predicate: external necessitation rule, internal modus ponens rule, and positive introspection. No incompleteness theorem is needed here.

If $S⊢G$, necessitation rule gives $S⊢\square G$. The displayed Gödel sentence equivalence also gives $S⊢\neg \square G$. These two theorems contradict the assumption that $S$ is a consistent first-order theory. ThereforeFor this part alone, the external necessitation rule condition suffices; the stronger internal conditions are used in the next part.

An arithmetic theory is one-consistent if there is no bounded arithmetic formula $\delta (x)$ for which it proves $\exists x\delta (x)$ and also proves $\neg \delta (\overline{n})$ for every standard natural number $n$. A finite tuple of existential witnesses can be coded by one natural number. The associated Sigma-1 soundness property says that every ${\Sigma }_1$ sentence it proves is true in the standard natural numbers.

Suppose first that the theory is one-consistent, but proves a false ${\Sigma }_1$ sentence $\exists x\delta (x)$. For every standard $n$, $\neg \delta (\overline{n})$ is then a true bounded sentence. Bounded completeness makes each such sentence a theorem, violating one-consistency.

Conversely suppose the theory is ${\Sigma }_1$-sound. If it proved both the existential sentence and every negated standard instance, soundness would supply an actual witness $n$. Its positive instance $\delta (\overline{n})$ is a true bounded sentence and hence provable. Together with the assumed negative instance this would make the theory inconsistent; an inconsistent theory proves a false ${\Sigma }_1$ sentence, contrary to soundness. Thusunder the stated bounded-completeness assumption. In particular either condition implies that the theory is a consistent first-order theory.

Pi-1 soundness means that every closed Pi-1 theorem is true in the standard natural numbers. Consistency plus bounded completeness implies it, since a false universal bounded statement has a standard counterexample whose arithmetic verification is provable. It is weaker than full soundness and does not prevent a consistent arithmetic theory from proving a false Sigma-1 sentence.

A formula separates the number set $A$ from $B$ in $S$ if the displayed numeralwise proof implications hold. No decision is required outside $A\cup B$. In a consistent theory the sets must be disjoint. A diagonal sentence asserting the negation of its membership in a separator of provable from refutable codes is undecidable by the two direct contradiction cases.

Consider extending $S+{\mathrm{Con}}_S$ by a rule sending every ${\mathrm{Con}}_A$ to ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. Put $A=S+\neg {\mathrm{Con}}_S$. The initial consistency axiom proves ${\mathrm{Con}}_A$ by the negated-consistency extension theorem, so the rule proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. But ${\mathrm{Con}}_A\to {\mathrm{Con}}_S$ is provable by inclusion of proofs, making $A+{\mathrm{Con}}_A$ inconsistent. Arithmetic verifies its finite contradiction proof. Thus the unrestricted rule proves both that theory's consistency and inconsistency. This differs from an externally justified progression along specified sound theories.

A witness constant is a fresh constant symbol added to a first-order language so that an existential assertion has a named witness. In a Henkin construction one adds $\exists x\theta (x)\to \theta (c_{\theta })$, with $c_{\theta }$ absent from the previous language. Freshness preserves consistency. Repeating the construction for the successively enlarged languages supplies the witness property used in a term model.