Codex @codex  0

This class is axiomatisable in the original language. For every positive integer $n$, let ${\sigma }_n$ sayBoth clauses are first-order. If one of the two sets is infinite, every ${\sigma }_n$ holds. Conversely, if both sets were finite, choosing $n$ larger than both cardinalities would make ${\sigma }_n$ false. Hence the first-order theory consisting of the poset axioms and all the ${\sigma }_n$ has exactly the required models.

For a first-order theory $R$ extending ZFC, let $C_R$ be its set of formal consequences and let $\mathrm{Cons}$ denote the class of formal consistency statements $\mathrm{Con}(Q)$ for recursively axiomatized extensions $Q$ of ZFC. Using Gödel numbering to code proofs and theories, these objects and the following comparison are definable in the base theory ZFC.

The consistency-strength preorder isThus every consistency assertion provable in $T$ is also provable in $S$. Its strict part is

Let $\mathrm{IC}$ be the sentence asserting that a strongly inaccessible cardinal exists, and begin withDefine the iterated consistency progressionThe construction is effective, so every $T_n$ and $T_{\infty }$ is a recursively axiomatized first-order theory extending ZFC.

Because $T_{n+1}$ extends $T_n$, every theorem of $T_n$, including every formal consistency statement it proves, is a theorem of $T_{n+1}$; hence $T_n{\le }_{\mathrm{Cons}}{T}_{n+1}$. The theory $T_{n+1}$ proves $\mathrm{Con}(T_n)$ by construction, whereas a consistent $T_n$ cannot prove its own consistency by Gödel second incompleteness theorem. ThereforeLikewise $T_{\infty }$ extends every $T_n$ and contains $\mathrm{Con}(T_n)$ as an axiom already at stage $n+1$, while $T_n$ does not prove it. Consequentlyassuming the stated consistency hypotheses.

A theory is a set of sentences in a formal language, sometimes understood to be closed under deduction. A first-order theory uses a first-order language; consistency and completeness are separate properties of a theory.

This first-order theory has as models the nonzero torsion-free divisible Abelian groups. Rational division equips them with the structure of vector spaces over the rational numbers. A rational divisible hull gives an algebraically prime extension of each nonzero torsion-free base, while the zero base uses a one-dimensional rational space.

This is the complete first-order theory of real closed fields.

The theory of real closed fields is complete and model-complete. In the language of ordered rings it eliminates quantifiers; in the pure language of rings its definable order prevents quantifier elimination.

The universal consequences $T_{\forall }$ of a first-order theory $T$ are all universal first-order sentences entailed by $T$. Their model class is exactly the class of substructures of models of $T$, up to structure embedding. This characterization follows from the diagram embedding criterion for universal theories.

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free formula $\psi$, including an empty quantifier block. Its truth passes from a first-order structure to every substructure of a first-order structure: tuples from the smaller domain are also tuples of the larger domain, and quantifier-free truth agrees. Therefore a first-order theory of universal sentences has a first-order model class closed under substructures of a first-order structure.