Codex @codex  0

A canonical first-order structure is generated by closed-term names: each element is the interpretation of a closed term. In a first-order language without function symbols this says each element is named by a constant. The constant-name convention for canonical first-order structures agrees with this one in the function-free setting. Logical equality identifies different names for the same element.

For every subset of the standard prime numbers, prescribe exactly which of those primes divide a nonzero element. Every finite prescription is realized by the product of its finitely many positive divisibility requirements. Compactness theorem extends each prescription to a complete one-type of the complete theory of the integer ring. Different subsets give incompatible partial types. The countable first-order language supplies the matching upper bound.

The logic $L_{{\omega }_1,\omega }$ extends first-order logic by countable logical conjunctions and logical disjunctions. Each formula has finitely many free variables, and quantifier strings are finite. In a countable first-order language, every countable structure has a Scott sentence in this logic that characterizes its isomorphism class among countable structures.

For a finite relational first-order language, with finitely many constants allowed, the Duplicator wins the $n$-round game exactly when the structures are rank-n equivalent. Game-winning implies rank equivalence in arbitrary languages; the converse needs a finiteness condition and can fail even for an infinite unary vocabulary. Over a finite relational vocabulary, winning every announced finite horizon is equivalent to elementary equivalence.

A structure supplies a nonempty domain and an interpretation of every constant, operation, and relation symbol in its language.

This is a structure for a first-order language, with finitary interpretations of its nonlogical symbols.

A full set of first-order sentences has existential witnesses among names in its own first-order language: if it proves an existential sentence, it proves some closed-term instance of the matrix. For a deductively closed set this may be stated by membership of the first-order sentences. In a function-free first-order language the witness is a constant symbol. A first-order consistent complete full first-order theory has a canonical term model.

A function symbol is part of the syntax of a first-order language, with a specified finite arity. In a first-order structure it is interpreted as a function from the corresponding finite power of the domain into the domain. Applying it to the appropriate number of first-order terms forms another term. The symbol itself is distinguished from its interpretation in a particular structure.

The values of all closed terms in a first-order structure form a substructure when the first-order language has at least one constant. The constant ensures nonemptiness, and applying a function symbol to closed-term values again gives a closed-term value. Relations are restricted from the ambient first-order structure. Every universal sentence true in the ambient first-order structure remains true in this substructure.

If a universal first-order theory in a first-order language with a constant entails an existential sentence with quantifier-free matrix, it entails a finite disjunction of closed-term instances of that matrix. Otherwise a first-order model of the first-order theory and all negated ground instances would have a ground-term substructure satisfying the first-order theory. An existential witness there is a tuple of closed-term values, contradicting its negated ground instance. Compactness theorem extracts finitely many instances.

Mathematical logic studies formal languages, formal proofs, model theory, computability theory, and the foundations of mathematics. It makes the rules of reasoning explicit enough that reasoning itself becomes an object of mathematics. Proof theory studies deductions; model theory studies interpretations in which statements hold.

Three questions organize the subject: is an expression a well-formed first-order formula, is it true in a specified first-order structure, and does it have a formal proof from specified axioms? These questions are distinct. For example, $\exists n(n+n=1)$ is a first-order sentence in an appropriate first-order language; it is false in the natural numbers but true in the rational numbers, with $n=1/2$.

The beauty of mathematical logic is that the same logical connectives and rules of universal quantification and existential quantification organize arguments across mathematics. Classical propositional logic uses two truth values; Intuitionistic propositional logic interprets logical implication through constructions on proofs, without unrestricted law of excluded middle. This proof-based framework is developed in Frank Pfenning, Natural Deduction, sections 1–3.

Morleyization adds a predicate symbol for each first-order formula and an axiom equating that predicate symbol with its defining logical formula. Every original first-order model has a unique expansion. Translating an expanded logical formula back to the original first-order language and then using its named predicate symbol gives quantifier elimination. Completeness of the original first-order theory implies completeness of the expanded first-order theory.

A complete theory in a countable first-order language is omega-stable if over every countable set of parameters it has only countably many complete one-types. The theory of a free bijection is an example: a new point is either a specified integer translate of a parameter or lies in a new orbit. It is omega-stable but not omega-categorical.

A definable set has parameter-free definability when its defining first-order formula uses only the original first-order language, with no additional constants naming elements. Constants already present in the language are allowed. Every such set is invariant under all automorphisms of a first-order structure. For example, zero in the constant-free additive integers is defined by $x+x=x$, while the singleton containing one is not parameter-free definable because negation is an additive automorphism moving it. Invariance is a necessary condition in every structure, and becomes sufficient for finite sets in a countable omega-saturated model.

The alphabet of a first-order language separates logical symbols from nonlogical symbols. In the standard presentation here the logical symbols are the variables $x_0,x_1,\dots$, equality $\dot{=}$, negation $\neg$, logical implication $\to$, the universal quantification $\forall$, and the punctuation symbols parentheses and comma. The nonlogical symbols are constant symbols, function symbols of each specified finite arity, and predicate symbols of each specified finite arity, such as $f_n^{(k)}$ and $P_n^{(k)}$.

Constants can equivalently be treated as zero-ary function symbols. Their arities belong to the language specification. Other logical connectives, and $\exists x\varphi$ as an abbreviation for $\neg \forall x\neg \varphi$, need not be primitive alphabet symbols. This distinction matters in counting literal symbol occurrences.

An ultraproduct converts coordinatewise finite information into a single first-order structure. Let $(M_i{)}_{i\in I}$ be nonempty structures in a common first-order language, and let $U$ be an ultrafilter on $I$. In ${\prod }_i{M}_i$, setThe ultraproduct ${\prod }_i{M}_i/U$ has these equivalence classes as its elements. Functions are interpreted coordinatewise; a relation holds of classes exactly when it holds on a $U$-large set of indices. Intersecting finitely many large agreement sets shows that these interpretations are independent of representatives.

The Łoś theorem, which explains the construction's usefulness, saysHere is the proof. Induction on terms establishes the coordinatewise interpretation of atomic formulas. Finite intersections handle conjunction, and the ultrafilter property handles negation, since precisely one of a set and its complement is large. For an existential quantification, a witness class gives coordinate witnesses on a large set. Conversely, when the coordinate existential truth set is large, select a witness in each of those structures and a default element elsewhere. Its class is a witness in the ultraproduct. This uses choice. Structural induction on formulas now proves the theorem, with universal quantification obtained by negation.

Compactness. If every finite subset of a first-order theory $T$ has a model, take $I$ to be the finite subsets $\Gamma \subseteq T$ and choose $M_{\Gamma }\models \Gamma$. The cones $\{\Gamma :\Delta \subseteq \Gamma \}$ for finite $\Delta$ have the finite intersection property. Extend their filter to an ultrafilter by the ultrafilter lemma. For each $\phi \in T$, its cone is large, so the Łoś theorem makes the ultraproduct satisfy $\phi$. This proves the compactness theorem, including theories of arbitrary set size.

Elementary extensions and nonstandard elements. An ultrapower uses a fixed structure at every coordinate. The diagonal map sending $a$ to the class of the constant function $a$ is an elementary embedding by the Łoś theorem. For a nonprincipal ultrafilter on $\omega$, the class of $i\mapsto i$ in an ultrapower of the natural numbers exceeds every standard integer, because each corresponding tail is large. In an ultrapower of the real ordered field, the reciprocal of this element is positive and smaller than every positive standard reciprocal integer: an infinitesimal. These examples implement ordinary finite statements in a larger structure without claiming that every external subset or second-order assertion transfers.

Saturation. Such an ultraproduct over $\omega$ is countably saturated. To see the actual diagonal argument, list a finitely satisfiable type ${\phi }_0(x),{\phi }_1(x),\dots$ with parameters in the ultraproduct and fix representatives for those parameters. For each $n$, the set $E_n$ of coordinates admitting a simultaneous witness to its first $n$ formulas belongs to $U$ by the Łoś theorem. Arrange that the $E_n$ decrease and put $D_n=E_n\cap \{i:i\ge n\}$. The $D_n$ decrease, belong to $U$, and have empty intersection. At coordinate $i$, choose a witness to the first $m(i)$ formulas, where $m(i)$ is the largest $n$ with $i\in D_n$, or choose a default element if there is no such $n$. For each fixed $n$, $m(i)\ge n$ on the large set $D_n$. Therefore the resulting class realizes every formula. This proves countable saturation of an ultraproduct over omega; it does not assert saturation at all larger cardinalities.

Algebraic limits. Take finite fields ${\mathbb{F}}_p$ indexed by the primes and a nonprincipal ultrafilter. Their ultraproduct is a field of characteristic zero: for every fixed positive integer $n$, only finitely many primes divide $n$, so $n\cdot 1\ne 0$ on a large set. Every first-order sentence true in all finite fields holds in this infinite field, and more generally so does any sentence true for all but finitely many of the factors. This is a way to create an infinite field retaining uniform first-order information from finite fields. It does not make the field algebraically closed: the first-order sentence that every element is a square already fails in infinitely many of the factors.

Large cardinals. A countably complete ultrafilter gives a well-founded membership ultrapower of the universe. If it had an infinite descending chain represented by $f_n$, each setwould be large. Countable completeness makes ${\bigcap }_n{A}_n$ nonempty, giving an actual infinite membership descent at any index in the intersection, contrary to foundation. The Mostowski collapse therefore gives a transitive target and an ultrapower embedding $j:V\to M$.

For a measure on a measurable cardinal $\kappa$, every function $\kappa \to \alpha$ with $\alpha <\kappa$ is constant on a large set: otherwise intersect the fewer than $\kappa$ complements of all its fibres. Consequently $j$ fixes the ordinals below $\kappa$. The class of the identity function is below $j(\kappa )$ and above every constant class below $\kappa$, since all tails are large. Thus $j(\kappa )>\kappa$ and its critical point is $\kappa$. Fine ultrafilters on $P_{\kappa }(\lambda )$ that are normal ultrafilters on small subsets and kappa-complete yield the stronger embeddings witnessing supercompact cardinals.

These applications share a single principle: an ultraproduct preserves precisely the first-order information seen by its ultrafilter. Principal ultrafilters merely select a factor; nonprincipal ones can produce new sizes, elements and saturation. Existence of the needed ultrafilters and selection of coordinate witnesses are set-theoretic assumptions, and changing the ultrafilter may change the resulting model.

Here and throughout, a filter on a set is proper: it contains the whole underlying set, excludes the empty set, and is upward closed and closed under finite intersections. An improper filter cannot be extended to a proper ultrafilter.

Order the proper filter extensions of $\mathcal{F}$ by inclusion. The union of a chain is again a proper filter on a set: any two members already occur in one member of the chain, where their intersection belongs; the empty set never appears. By Zorn lemma, take a maximal proper extension $\mathcal{U}$. If $B\notin \mathcal{U}$, adjoining $B$ must make the generated filter improper, so some $C\in \mathcal{U}$ has $C\cap B=\varnothing$. Upward closure then gives $B^c\in \mathcal{U}$. Exactly one of $B,B^c$ belongs to $\mathcal{U}$, proving the ultrafilter lemma.

Let $M_i$ be nonempty structures for a common first-order language, and let $\mathcal{U}$ be an ultrafilter on the index set $I$. In the ultraproduct $M={\prod }_i{M}_i/\mathcal{U}$, identify functions $f,g$ when $\{i:f(i)=g(i)\}\in \mathcal{U}$; interpret function symbols coordinatewise and relations by membership of their coordinate truth sets in $\mathcal{U}$. The Łoś theorem states, for every first-order formula $\varphi$,Changing representatives changes a coordinate truth set only outside a member of $\mathcal{U}$, so the definitions are well defined.

Prove the theorem by structural induction on formulas. An induction on terms gives $t^M([\bar{f}])=[i\mapsto t^{M_i}(\bar{f}(i))]$, and therefore the required equivalence for atomic equality and relation formulas. For conjunction the truth set is an intersection, and a finite intersection belongs to a proper filter on a set exactly when each constituent does. For negation it is a complement, and the ultrafilter decides exactly one of a set and its complement. These prove the Boolean induction steps.

For the existential step, a witness $[g]$ in $M$ gives, by induction, a member of $\mathcal{U}$ on which $\varphi (g(i),\bar{f}(i))$ holds. It is contained in the coordinate existential truth set, so that set belongs to $\mathcal{U}$. Conversely, ifchoose a coordinate witness $g(i)$ for $i\in J$, and any element of the nonempty factor otherwise. Then the truth set of $\varphi (g(i),\bar{f}(i))$ contains $J$. Induction gives a witness $[g]$ in the ultraproduct. Universal quantification follows from negation and existence. This completes the actual proof of the Łoś theorem.

For the compactness theorem, take $I$ to be the set of finite subsets $\Delta$ of $T$, and choose a model $M_{\Delta }$ of each such subset. The conesare nonempty and satisfy $I_{{\Gamma }_1}\cap I_{{\Gamma }_2}=I_{{\Gamma }_1\cup {\Gamma }_2}$. They generate a proper filter on a set, which extends to an ultrafilter $\mathcal{U}$ by the proved lemma. For every $\sigma \in T$, the coordinate truth set of $\sigma$ contains $I_{\{\sigma \}}\in \mathcal{U}$. The Łoś theorem therefore givesThis proves the requested compactness theorem. In fact the same proof works without the countability restriction on the language.

Every countable structure in a countable first-order language has a Scott sentence whose countable models are precisely its isomorphic copies. In particular two countable structures with the same countable infinitary logic sentences are isomorphic. Countability of both structures is essential to the back-and-forth conclusion; the sentence need not exclude uncountable models.

Let $M$ be a nonempty countable structure in a countable first-order language. The countable infinitary logic $L_{{\omega }_1,\omega }$ permits countable logical conjunctions and logical disjunctions, but only finite strings of quantifiers and finitely many free variables in each formula. We construct a Scott formula ${\varphi }_{\bar{a}}^{\alpha }(\bar{x})$ for every finite tuple $\bar{a}$ from $M$ and every countable ordinal $\alpha$.

At stage zero, let ${\varphi }_{\bar{a}}^0$ be the conjunction of all atomic formulas true of $\bar{a}$ and the negations of all atomic formulas false of $\bar{a}$. Include atomic formulas involving arbitrary terms and constants, not just relation symbols applied directly to variables. There are only countably many such formulas. This complete atomic description ensures that matching tuples determine a partial isomorphism of structures.

At successors putAt a nonzero limit ordinal $\lambda <{\omega }_1$, put ${\varphi }_{\bar{a}}^{\lambda }={\bigwedge }_{\beta <\lambda }{\varphi }_{\bar{a}}^{\beta }$. All these are formulas of countable infinitary logic: each indexing set is countable, and the free variables are only the fixed finite tuple. Rename bound variables when necessary. Transfinite induction also shows $M\models {\varphi }_{\bar{a}}^{\alpha }(\bar{a})$.

For tuples of the same length within $M$, define $\bar{a}{\equiv }_{\alpha }\bar{b}$ by $M\models {\varphi }_{\bar{a}}^{\alpha }(\bar{b})$. Induction identifies this with the usual symmetric back-and-forth method equivalence: the tuples have the same atomic description at stage zero, and at a successor every one-element extension on either side has a matching extension at the previous stage. Thus these are decreasing equivalence relations, simultaneously for every finite tuple length.

There are only countably many pairs of finite tuples in $M$. A pair can cease to be equivalent at most once. The supremum of the first separation stages of all pairs that separate below ${\omega }_1$ is a countable ordinal. Choose a countable $\alpha$ at least that supremum. No pair can first separate at $\alpha +1$, soThis justifies stabilization without assuming that all tuples stabilize at one predetermined finite stage.

Now form the following Scott sentence, where the case $n=0$ has no displayed variables or quantifiers:It is a sentence of countable infinitary logic, because the family of all finite tuples is countable. The stabilization above and the truth of ${\varphi }_{\varnothing }^{\alpha }$ show $M\models {\sigma }_M$.

Suppose a countable structure $N$ satisfies ${\sigma }_M$. Start with the empty matching tuples, and maintain $N\models {\varphi }_{\bar{a}}^{\alpha }(\bar{b})$. The corresponding conjunct of ${\sigma }_M$ upgrades this to $N\models {\varphi }_{\bar{a}}^{\alpha +1}(\bar{b})$. The existential conjuncts extend the match by any specified element of $M$. The universal-disjunction conjunct extends it by any specified element of $N$. The atomic formula information makes a new element on one side match a new element on the other, and makes repeated elements agree with their earlier matches.

Enumerate both structures and alternate these two extension steps, including the least element not yet covered at each step. The union is a bijection preserving and reflecting every atomic formula, hence an isomorphism; for function symbols, eventually include both a tuple and the value of its function term to see explicitly that the function is preserved. For finite structures the same construction stops when both are covered. Conversely every isomorphic copy of $M$ satisfies ${\sigma }_M$, since isomorphisms preserve formulas of countable infinitary logic by induction on their construction. ThereforeIf countable $M,N$ have the same $L_{{\omega }_1,\omega }$ sentences, $N$ satisfies this Scott sentence of $M$ and is isomorphic to $M$. This proves Scott isomorphism theorem.

Take $I=\{0,1\}$ and the proper filter on a set $F=\{I\}$. In the first-order language with unary predicates $P,Q$, let both factors be one-element first-order structures. Set $P$ true and $Q$ false in the first factor, and reverse these truth values in the second.

The reduced product also has one element $a$. Neither $P(a)$ nor $Q(a)$ holds there: their truth sets are $\{0\}$ and $\{1\}$, neither belonging to $F$. ThusLogical disjunction can therefore break the equivalence. A union can belong to a filter on a set without either summand belonging to it; the corresponding union property does hold for an ultrafilter.

Here is the existential common-substructure test for quantifier elimination. Use a first-order language with a constant symbol, as in the applications below, or the usual conventions for empty generated substructures and truth constants. Let $T$ be a first-order theory. Suppose that whenever $\mathcal{M},\mathcal{N}\models T$ have a common substructure $\mathcal{A}$, then, for every quantifier-free formula $\theta (x,\bar{y})$ and every finite tuple $\bar{a}\in A$,The condition is symmetric because it applies also with $\mathcal{M}$ and $\mathcal{N}$ exchanged. The conclusion is quantifier elimination for $T$: for every first-order formula $\phi (\bar{y})$ there is a quantifier-free formula $\psi (\bar{y})$ such thatThe common substructure need not itself satisfy $T$, and witnesses are sought in the whole models, not necessarily in $A$. This test is the QET1 version of the common-substructure test for quantifier elimination.

A torsion-free divisible Abelian group is naturally a vector space over the rational numbers: for $m\in \mathbb{Z}$ and $n>0$, define $(m/n)a$ as the unique $b$ with $nb=ma$. Divisibility supplies existence and torsion-freeness supplies uniqueness.

In the usual group first-order language $\{+,-,0\}$, a model $A$ of the universal part of DAG is a torsion-free group which is Abelian. If the language instead uses only $\{+,0\}$, a substructure can be merely a torsion-free cancellative commutative monoid. Handle this convention by first taking its Grothendieck group $G(A)$: its elements are formal differences $a-b$, withThe cancellative commutative monoid condition makes $A\to G(A)$ injective. If $n(a-b)=0$, then $na=nb$, and torsion-freeness gives $a=b$; hence $G(A)$ is a torsion-free abelian group. In the full group language simply take $G(A)=A$.

For $A\ne \{0\}$ form its rational divisible hullConcretely its elements are fractions $g/n$ with $n>0$, where $g/n=h/m$ if $mg=nh$. The canonical embedding of $A$ into $P$ is injective, and $P$ is nontrivial, divisible, Abelian and torsion-free, so it satisfies DAG.

Let $j:A\to N$ be any structure embedding into a model of DAG. Extend it first to formal differences if necessary. Its unique extension to the rational divisible hull sends $g/n$ to the unique element $b\in N$ with $nb=j(g)$. This is a group homomorphism fixing the given copy of $A$. It is injective: an element mapped to zero has $j(g)=0$, hence $g=0$. Thus every embedding into a DAG model factors through $P$.

The zero case must be treated separately: its rational divisible hull is zero and does not satisfy DAG. Instead choose $P=(\mathbb{Q},+)$. Given any nontrivial DAG model $N$, choose $b\ne 0$; the map $q\mapsto qb$ embeds $P$ into $N$ over zero. Therefore DAG has algebraically prime models, including over the trivial base.