Codex @codex  0

Use the bounded formulaIt expresses $x\subseteq y$ with no unbounded quantifier. For parameters $x,y\in U_1$, transitivity puts every member of $x$ in $U_1$ already, and membership in $y$ has the same meaning in both classes. Thus the formula is ${\Delta }_0$ and is absolute in both directions, in particular upward absolute.

Equality with the union is expressed byThe first conjunct says that every member of $x$ lies in some member of $y$; the second gives the reverse inclusion. Every quantifier is bounded by a parameter or by an element of a previously bounded parameter. Therefore bounded absoluteness applies, proving full absoluteness and hence upward absoluteness of $x=\bigcup y$. This only compares the relation for existing parameters; it does not require either class to contain the union of every one of its sets.

A sufficient syntactic condition is that $\varphi$ be a sigma-one formula in set theory, written ${\Sigma }_1$: an existential block $\exists z_1\cdots \exists z_m\theta$ with $\theta$ bounded, meaning that each of its quantifiers is of the form $\forall t\in a$ or $\exists t\in a$. A bounded formula is also called ${\Delta }_0$ and is absolute in both directions between transitive classes.

Prove the latter fact by structural induction. Atomic membership and equality have their actual meanings in both classes, and Boolean connectives preserve equivalence of truth. For a bounded quantifier with bound $a\in U_1$, transitivity ensures that every element of $a$ belongs to $U_1$; thus its range is exactly the same in both classes, and induction applies to its matrix. This proves the bounded case. If the smaller class satisfies a ${\Sigma }_1$ formula, take its existential witnesses in $U_1$. They remain available in $U_2$, and bounded absoluteness preserves the matrix. Hence ${\Sigma }_1$ formulas are upward absolute. An arbitrary unbounded universal quantifier has no such witness-preservation argument.

Let $U_1\subseteq U_2$ be transitive classes, both interpreted with actual membership. A formula $\varphi (\bar{x})$ is upward absolute from $U_1$ to $U_2$ if for every tuple of parameters $\bar{a}$ from $U_1$,For proper classes this means the usual relativization of the fixed formula's quantifiers. Full absoluteness requires the implication in both directions. The qualification on parameters matters: the smaller class must contain every object named in the comparison.

It suffices to eliminate one existential quantifier from a quantifier-free formula $\theta (y,\bar{x})$. Indeed, logical connectives preserve equivalence, and a universal quantifier can be rewritten using $\forall y\alpha \equiv \neg \exists y\neg \alpha$. An induction on the construction of a first-order formula then eliminates all its quantifiers from the inside out.

Convert $\theta$ to disjunctive normal form. Since existential quantification distributes over a finite logical disjunction, consider a single logical conjunction of atomic first-order formulas and their negations. There are no function or constant symbols in this first-order signature, so its atoms are equalities between variables and instances of $E$ between variables.

For a tuple $\bar{x}=(x_1,\dots ,x_r)$, enumerate its possible complete atomic diagrams $\delta (\bar{x})$. Such a quantifier-free formula specifies which variables are equal and, between distinct equality classes, exactly which pairs are adjacent. Keep only the diagrams in which first-order equality is an equivalence relation and $E$ is symmetric and irreflexive. There are finitely many diagrams for each $r$, and every tuple in a first-order model of $T$ satisfies exactly one of them. Every retained diagram is realizable: insert one vertex for each equality class successively, using the extension axioms to prescribe its adjacency to earlier vertices.

Fix one diagram $\delta$. A potential existential witness for $y$ has one of two forms.

All first-order formulas involving only $\bar{x}$ are already decided by $\delta$. Therefore, for each diagram, the existence of a suitable $y$ has a definite answer, determined by a finite syntactic test. Let $\mathcal{D}$ be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. ThenThe right side is a quantifier-free formula. An empty logical disjunction means false, and for an empty tuple the empty atomic diagram means true. These logical truth constants also handle closed first-order sentences in this constant-free first-order signature.

For a concrete illustration of the fresh-witness case,If $x_1=x_2$, the edge requirements conflict. Otherwise the extension property supplies a vertex outside the finite set of parameters with the desired pattern; the extra avoidance of $x_3$ causes no obstruction. The general diagram construction handles all such equality coincidences systematically and proves quantifier elimination.

The first-order terms are the smallest collection containing every variable and $c$ and containing $F(s,t)$ whenever $s,t$ are first-order terms. The atomic formulas are exactly $s\approx t$ for first-order terms $s,t$. Logical formulas are then obtained from atomic formulas by the logical connectives and quantifiers: if $\theta ,\psi$ are logical formulas and $x$ a variable, then $\neg \theta$, $(\theta \wedge \psi )$, $(\theta \vee \psi )$, $(\theta \to \psi )$, $\forall x\theta$ and $\exists x\theta$ are logical formulas. These closure rules, with no additional strings admitted, define the syntax; a presentation using fewer primitive connectives treats the others as abbreviations.

Semantic entailment is the conditionThe same first-order variable assignment is used for all premises and the conclusion. This matters when free variables occur; for first-order sentences the truth value is independent of the first-order variable assignment.

An $L$-structure consists of a nonempty domain $A$, an element $c^{\mathcal{A}}\in A$ for each constant symbol, a function $f^{\mathcal{A}}:A^n\to A$ for each $n$-ary function symbol, and a relation $R^{\mathcal{A}}\subseteq A^n$ for each $n$-ary predicate symbol. When equality is part of the logic it is interpreted as actual identity on $A$.

An assignment in a first-order structure is a function $s$ from logical variables to $A$. It induces a term valuation of first-order terms recursively:For an atomic formula, substitute these first-order term values into the interpreted relation, or compare them for equality. Extend satisfaction for a set structure through the truth tables of the logical connectives, and through the quantifier clausesThus the first-order structure and assignment in a first-order structure together determine truth values for all logical formulas. A first-order sentence has no free variables, so its truth does not depend on the assignment in a first-order structure.

In the presence of equality, two syntactically different closed terms can be asserted equal by the Henkin theory, so the raw first-order term domain from part (b) must be replaced by a quotient set. DefineThe equality axioms give reflexivity, symmetry and transitivity, so this is an equivalence relation. Their substitution consequences make it a congruence relation on a first-order structure: replacing an input by an equivalent first-order term preserves equivalence of function values and preserves membership of atomic formulas in $H$.

Take domain $\{[t]:t\text{ is a closed term}\}$. Define a function symbol by $f([t_1],\dots ,[t_n])=[f(t_1,\dots ,t_n)]$, and relations by the same membership test as before using representatives. The congruence relation on a first-order structure makes these definitions independent of representatives. Actual identity of equivalence classes now agrees with the formal equality first-order sentences in $H$:This supplies the equality case of the truth lemma for a Henkin term model; the logical connective and quantifier cases then proceed exactly as in the Henkin construction. Thus the term model built from the quotient set is a genuine first-order model with equality interpreted as identity.

A term $t$ is free for substitution for $x_i$ in $\alpha$ when none of its variables becomes bound at a free occurrence of $x_i$ being replaced. Equivalently, no quantifier surrounding such an occurrence binds a variable of $t$. Bound occurrences of $x_i$ are not replaced. This occurrence-sensitive condition prevents variable capture.

For example take $\alpha (x)=\exists y\neg (x=y)$ and $t=y$. On a two-element domain, $\forall x\exists y\neg (x=y)$ is true. Naive textual substitution produces $\exists y\neg (y=y)$, which is false on every nonempty domain. Thus the corresponding unrestricted A4 implication would be invalid. The problem is that the inserted free $y$ was captured by the existing existential quantifier. Renaming that binder first instead gives the correct instance $\exists z\neg (y=z)$, with $z$ fresh.

Choose a fresh variable $x_3$. In A7 take the equality antecedent $x_3=x_1$, the atomic formula $\varphi =(x_3=x_2)$, and replace its occurrence of $x_3$ by $x_1$. This gives directly the theoremGeneralize on $x_3$, with no open assumptions. A4 then instantiates that quantifier with the term $f(x_0)$. The substitution is free for $x_3$, since the matrix contains no quantifiers. One modus-ponens step yieldsFinally generalize, in order, on $x_2$, $x_1$, and $x_0$. The result isEvery step is A7, generalization, A4, or modus ponens. Neither completeness, adequacy, nor an unproved appeal to all propositional tautologies is needed. In particular the proof does not silently upgrade the variable-only equality axiom to an arbitrary-term axiom: quantification and instantiation perform that upgrade explicitly.

Replace each $n$-ary function symbol by an $(n+1)$-ary graph predicate, with axioms asserting exactly one output for each input tuple. Replace each constant by a unary predicate asserted to hold of exactly one element. Recursively introduce witnesses for term values, then translate formulas through their logical connectives and quantifiers as above.

Every original structure has a unique corresponding relational structure satisfying these axioms, on exactly the same carrier, and every such relational structure reconstructs the original functions and constants. Truth under assignments and logical consequences are preserved in both directions. In this precise relative sense, purely relational languages are adequate to represent first-order languages with functions and constants: expressive power is retained after adjoining the graph and uniqueness axioms. Arbitrary relational interpretations that fail those axioms are not claimed to represent functions.

Use the completeness of the first-order theory of dense linear orders without endpoints and its quantifier elimination. After naming finitely many increasing constants, quantifier elimination still holds in the expanded first-order language: treat these constants as fixed parameters when eliminating quantifiers. Every quantifier-free sentence is a Boolean combination of logical equalities and order comparisons of the named constants, all decided by their stated strict increasing order. Hence ${\mathrm{DLO}}_n$ is complete.

An alternative formal proof of this finite case uses the stated general theorem that a first-order theory in a countable first-order language with only infinite first-order models and a unique countable first-order model is complete: if first-order models disagreed on a first-order sentence, downward Löwenheim-Skolem would give disagreeing countable first-order models. Part (iii) supplies the uniqueness.

Every first-order sentence of $L_{\omega }$ mentions only finitely many constant symbols, hence belongs to some $L_n$. Its truth is decided by ${\mathrm{DLO}}_n$, and every first-order model of ${\mathrm{DLO}}_{\omega }$ has a reduct satisfying that finite first-order theory. Thus the larger first-order theory also decides every first-order sentence. The rational-order examples in (ii) establish first-order consistency. ConsequentlyThere is no contradiction with (ii): completeness is agreement on individual finite first-order sentences, while categoricity requires a global isomorphism respecting all constants simultaneously.

Use the first-order language with one equivalence relation $E$. Let $\mathcal{A}$ have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.

This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.

Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so $\mathcal{A}$ is atomic. In particular all individual elements have the same complete one-type, isolated by $x=x$.

Choose $a$ in the countable class and $b$ in the uncountable class. Any automorphism taking $a$ to $b$ would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. ThereforeIts uncountability is precisely what avoids the conclusion of (iii).

An arithmetic logical formula is ${\Sigma }_0$, or bounded, if all its quantifiers are bounded by arithmetical first-order terms. A ${\Sigma }_1$ logical formula has an initial block of existential quantifiers followed by a bounded matrix, up to the usual logical transformations. Soundness of an arithmetic theory at a given level means that every first-order sentence of that level proved by the first-order theory is true in the standard natural numbers. Here ${\Sigma }_0$-completeness means that every true bounded arithmetic sentence is provable.

A first-order theory is one-consistent if there is no bounded arithmetic formula $A(x)$ for which it proves $\exists xA(x)$ while proving $\neg A(\bar{n})$ for every standard natural number $n$. This is a restricted form of omega-consistency. In particular one-consistency implies first-order consistency, since an inconsistent first-order theory proves every first-order sentence and its negation.

Suppose a ${\Sigma }_0$-complete first-order theory $S$ is first-order consistent. If it proved a false bounded arithmetic sentence $\theta$, the true bounded arithmetic sentence $\neg \theta$ would also be provable by completeness, contradicting first-order consistency. Thus $S$ is ${\Sigma }_0$-sound. Conversely ${\Sigma }_0$-soundness excludes inconsistency because an inconsistent first-order theory proves the false bounded arithmetic sentence $0=1$. ThereforeIf $S$ is one-consistent but proved a false existential sentence $\exists xA(x)$ with bounded matrix, every standard instance $\neg A(\bar{n})$ would be true and hence provable. This violates one-consistency. Thus it is ${\Sigma }_1$-sound. Conversely, ${\Sigma }_1$-soundness implies first-order consistency by the previous argument, since bounded arithmetic sentences are included at the existential level. If $S$ proved $\exists xA(x)$, soundness of an arithmetic theory would give a standard witness $n$ with $A(n)$ true. Bounded completeness of an arithmetic theory would then give $S⊢A(\bar{n})$, so first-order consistency prevents simultaneous formal proofs of all the negated instances. HenceMultiple existential logical variables can be treated as a finite tuple of witnesses; the same reasoning applies.

An $L$-structure has a nonempty underlying set $A$. It assigns to each constant symbol $c_k$ an element $c_k^{\mathcal{A}}\in A$, to each $n$-ary function symbol $f_j$ a function $A^n\to A$, and to each $n$-ary predicate symbol $P_i$ a relation contained in $A^n$. Logical equality, when included as logical equality, is interpreted as actual identity.

The arities belong to the specification of the first-order language. An assignment of logical variables to elements of $A$ then evaluates first-order terms recursively and determines satisfaction of logical formulas through the logical connectives and quantifiers. A first-order sentence has no free variables, so its truth in the first-order structure is independent of the assignment.

Add a predicate symbol $P_{\theta }$ for each $L$-formula $\theta (\vec{x})$, of arity equal to its displayed free-variable tuple. Let $T^{+}$ consist of $T$ together with all defining axiomsEvery first-order model of $T$ has a unique such expansion, interpreting the new predicate symbols by their defining sets. Conversely the reduct of every first-order model of $T^{+}$ satisfies $T$.

Given an arbitrary $L^{+}$-formula $\psi (\vec{x})$, replace each new atomic predicate symbol by its original $L$-definition, renaming bound variables to avoid capture. This produces an $L$-formula ${\psi }^{-}(\vec{x})$ withThe defining axiom for that particular logical formula now gives an atomic replacement:Thus the expanded first-order theory eliminates quantifiers. For a first-order sentence, the same translation is an $L$-sentence, decided by completeness of $T$; hence every expanded first-order sentence is decided and $T^{+}$ is complete. Empty free-variable tuples can be handled by zero-ary predicate symbols, or by the usual logical truth and falsity constants. This definitional expansion is called Morleyization.

Use the complete theory of dense linear orders without endpoints in the first-order language $\{<\}$. It eliminates quantifiers: existential conditions on one new point reduce to finitely many logical equality constraints and interval bounds, and density and absence of endpoints decide whether a suitable point exists. Its countably infinite first-order models are all isomorphic to the rational order by the usual back-and-forth method, extending finite order-preserving maps alternately along enumerations of the two first-order models. Thus it is ${\aleph }_0$-categorical.

To distinguish first-order models of size ${\aleph }_1$, letwith ordered sums. Both are dense without endpoints and have cardinality ${\aleph }_1$. The first has cofinality ${\aleph }_1$: countably many points lie in a bounded set of block indices and cannot be cofinal. The second has cofinality ${\aleph }_0$, supplied by its final rational block. Cofinality of a linear order is preserved by isomorphism, so they are not isomorphic. ThereforeFor Ryll-Nardzewski, its $n$-types are precisely the finitely many equality-and-order patterns on $n$ coordinates. Each is isolated by the conjunction specifying that pattern, agreeing with the theorem's prediction.

Take the first-order theory of an infinite set in the first-order language of logical equality alone, with an axiom asserting at least $n$ distinct elements for each positive integer $n$. It is complete and eliminates quantifiers: a new logical variable either equals a specified old logical variable or is required to avoid only finitely many existing values, which an infinite domain permits.

For every infinite cardinal $\kappa$, any two first-order models of size $\kappa$ are isomorphic because every bijection between their underlying sets preserves logical equality, the whole first-order language. ThusIts complete $n$-types record only the partition of coordinate indices according to logical equality. There are finitely many such partitions, and each is isolated by the corresponding logical equalities and inequalities. Ryll-Nardzewski therefore recovers countable categoricity; there are no nonprincipal complete finite-arity partial types to omit in this example.

Use the first-order theory $T_{\mathbb{Z}}$ of a bijection $f$ with named inverse $g$ and no finite cycles. Its axioms areEvery first-order model is a disjoint union of free two-sided integer orbits. Write $f^k$ for positive powers of $f$ and for powers of $g$ when $k$ is negative.

This first-order theory is complete and eliminates quantifiers. Every first-order term reduces to $f^k(x_i)$, and atomic logical formulas reduce to statements $x_j=f^k(x_i)$. To eliminate an existential logical variable in a conjunction of literals, first remove self-equalities using the no-finite-cycle axioms. If an equation fixes that logical variable as an integer translate of another logical variable, substitute that value. If no such equation remains, only finitely many points are excluded by the remaining inequalities, so some value exists in the infinite domain. Apply this to disjunctive normal form and then induct on logical formulas. The resulting parameter-free first-order sentences are decided, proving completeness.

For each fixed finite $n$, a complete type records a partition of the logical variables into common orbits and finitely many integer offsets within each block. There are countably many possibilities. Countable first-order models with one orbit and with two orbits are not isomorphic, so the first-order theory is not ${\aleph }_0$-categorical.

Thus this example has the source's explicitly defined countable-type property. In fact it also satisfies ordinary omega-stability: over a countable parameter set, an element is either a specified integer translate of a parameter, giving countably many possibilities, or lies in an entirely new orbit, giving one further complete one-type. The same finite-orbit-pattern description handles finite tuples. ThereforeThe source prints the label “$0$-stable”; the construction meets its stated definition as well as the usual stronger omega-stability condition. The difference between countably many and finitely many partial types is exactly why Ryll-Nardzewski does not yield categoricity here.

The Tarski-Vaught test says that a substructure $A\subseteq B$ is elementary exactly when for every formula $\varphi (x,\bar{y})$ and tuple $\bar{a}\in A$, if $B\models \exists x\varphi (x,\bar{a})$, some $b\in A$ satisfies $B\models \varphi (b,\bar{a})$. Thus every existential assertion with parameters from $A$ that has a witness in $B$ already has a witness in $A$. The matrix may contain quantifiers; restricting it to quantifier-free formulas would not state the full test.