First-order logic

First-order logic permits quantification over elements of a structure while its nonlogical symbols describe operations, constants, and relations.

The fragment uses finite conjunction, set-indexed disjunction and existential quantification, with equality and atomic relations. It is preserved under inverse image functors of geometric morphisms. The universal closure of an axiom is expressed by its variable context, not an unrestricted universal-quantifier constructor.

A set of sequents between geometric formulas over a many-sorted signature. Its geometric syntactic category and geometric syntactic topology yield its classifying topos. A model satisfies a sequent when the interpreted antecedent subobject is contained in the consequent in the indicated context.

A geometric quotient adds geometric sequents over the same signature. Quotients are compared modulo provable equivalence. In a syntactic site the extra sequents become additional covers, giving a subtopos of the original classifying topos. Stronger axioms correspond to a larger site topology and a smaller subtopos.

Objects are geometric formulas in context modulo provable equivalence. Morphisms are provably total, single-valued geometric relations; composition is existential conjunction. Conjunction and equality give finite limits. Interpreting formulas in a model gives a finite-limit-preserving functor, with the additional continuity condition supplied by the geometric syntactic topology.

A family of definable arrows covers a formula when the theory proves that their images jointly exhaust that formula. Such covers encode disjunction and existential quantification. The resulting site presents the classifying topos of the geometric theory. Adding geometric axioms adds covering sieves, yielding the duality between geometric quotients and subtoposes.

A geometric formula is built from atoms by finite conjunction, arbitrary small disjunction and existential quantification. Empty conjunction and disjunction give truth and falsity. In a Grothendieck topos, these constructions use finite limits, unions and images. Formula contexts have finitely many variables.

Regular logic has atomic formulas and equality, truth, finite conjunction and unrestricted existential quantification. Its categorical semantics uses regular categories: conjunction is intersection and existential quantification is image. Disjunction and falsity are not added as formula constructors in the regular fragment.

A regular theory has axioms that are sequents between regular formulas. It has a regular syntactic category and a classifying topos of sheaves for the regular coverage. Its regular formulas enjoy the disjunction property of regular theories when a finite disjunction is allowed as an outer coherent conclusion.

If a regular theory proves an outer coherent sequent $\varphi ⊢{\bigvee }_{i=1}^n{\psi }_i$ with all formulas regular, it proves $\varphi ⊢{\psi }_i$ for some $i$. In the classifying topos, the corresponding subobjects cover the representable associated with $\varphi$. Irreducibility of that representable and full faithfulness of the syntactic Yoneda embedding produce the desired derivation.

The regular syntactic category has regular formulas-in-context as objects and provably functional regular relations as arrows. It has finite limits and stable image factorizations, with existential quantification supplying images. The regular coverage on this category presents the classifying topos of the theory.

A regular formula is built using the constructors of regular logic, with a finite variable context. The image of a definable relation interprets an existential quantifier. Regular formulas remain regular after substitution, conjunction and existential quantification.

A Cartesian theory uses a many-sorted first-order signature and sequents between Cartesian formulas. The fragment contains equality, atomic relations, truth, finite conjunction and existential quantification with provably unique witnesses. It has a Cartesian syntactic category with finite limits, whose finite-limit-preserving functors classify its internal models. Arbitrary existential quantification, disjunction and falsity are not added as finite-limit constructors.

In the positive finite-limit convention, a Horn theory uses atomic finite-conjunction sequents; uniquely witnessed existential extensions remain Cartesian. Its models are the finite-limit-preserving functors out of its Cartesian syntactic category. This convention does not insert arbitrary existential witnesses or falsity as Cartesian constructors. Its classifier is the presheaf classifier of a Horn theory.

Internal Horn models are finite-limit-preserving functors out of the Cartesian syntactic category. Since that category has finite limits, these are exactly flat functors; the presheaf Diaconescu equivalence for geometric morphisms proves the classifying property. Equivalently the classifier is the covariant functor category on finitely presented set-based models.

Objects are Cartesian formulas-in-context modulo provable equivalence, and arrows are provably total single-valued Cartesian relations. Composition quantifies the unique intermediate tuple. Context concatenation, conjunction and equality give finite limits. Its canonical model interprets a formula as its own context subobject, so factorization of antecedent through consequent is exactly sequent derivability.

If a Cartesian sequent fails to factor its antecedent subobject $A\hookrightarrow C$ through its consequent, the covariant representable functor ${\mathcal{C}}_{\mathbb{T}}(A,-)$ is a set-valued countermodel. It preserves finite limits, and the element named by the antecedent inclusion belongs to the antecedent but cannot belong to the consequent. Hence validity in every set model implies Cartesian derivability.

A Cartesian formula is built from atoms and equality using truth, finite conjunction and uniquely witnessed existential quantification. Uniqueness is proved relative to the theory before admitting the quantifier. In a finite-limit category, such a quantified relation projects monomorphically into the remaining context, so its semantics needs no arbitrary image operation.

Coherent logic uses atomic formulas and equality, finite logical conjunctions and logical disjunctions, truth, falsity and existential quantification. Sequents are universally interpreted in a finite variable context. Its categorical semantics is provided by coherent categories, where conjunction is intersection, disjunction is finite union and existential quantification is image.

When $y$ is not free in $\theta$, the coherent quantifier obeys $\theta \wedge \exists y\varphi ⊣⊢\exists y(\theta \wedge \varphi )$. Categorically this is the interaction of existential images with pullback, ensuring stable image factorizations in a coherent category.

A coherent theory is a first-order signature with a set of coherent sequents as axioms. It has a coherent syntactic category containing a conservative syntactic model. Theories of groups, rings and integral domains admit coherent axiomatizations.

A coherent sequent true in all set models of a coherent theory is coherently derivable. A generic underivable sequent remains false after the Boolean cover by a generic quasi-closed subtopos. Slice over its nonzero Boolean counterexample to show classical consistency of the theory with a named tuple satisfying the antecedent and negated consequent. The Henkin construction then gives a set-valued countermodel. This argument does not assume that every Boolean topos has points.

Objects are coherent formulas in context and arrows are provably total, single-valued relations, modulo provable equivalence. Composition existentially eliminates the intermediate tuple. Conjunction constructs finite limits, existential formulas construct images and disjunction constructs finite unions. It is a coherent category.

The canonical model interprets each sort as its truth-context object, each operation by its term graph and each relation by its atomic subobject. A coherent formula is interpreted by its own formula-in-context object. Consequently a coherent sequent holds in this model exactly when it is derivable in the theory.

A coherent sequent is an implication $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common context. Its semantics is inclusion of the two interpreted subobjects of that context. The context is universally quantified outside the formulas.

A coherent formula is built from atomic relations and equality using $\top$, $\perp$, finite conjunction, finite disjunction and existential quantification. General negation and universal quantification are not constructors. Substitution of well-typed terms preserves coherent formulas.

In first-order logic with logical equality, $s=t$ asserts that the terms denote the same domain element. Logical equality is interpreted as identity rather than as an arbitrary binary predicate. Its natural deduction rules include reflexivity and substitution: equal terms can replace one another in a first-order formula, subject to capture-avoiding substitution. Double-negating logical equality atoms in a Gödel-Gentzen negative translation preserves these rules when the transported translated first-order formula is stable.

Intuitionistic first-order logic has the usual introduction and elimination rules for logical connectives, quantifiers and logical equality, but no unrestricted double-negation elimination or law of excluded middle. Its proofs retain the witness and logical disjunction information that can be lost in classical first-order logic.

For an atomic formula $P$ (including logical equality), put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Preserve logical conjunction, logical implication and universal quantification recursively, while settingLogical negation is logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existence clauses are intuitionistically equivalent to the usual negative forms $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$. Every translated first-order formula is stable by stability of a formula under double negation. In classical logic the translation is equivalent to the original first-order formula by mathematical induction and double-negation elimination.

The Gödel-Gentzen negative translation transforms $\Gamma {⊢}_{\mathrm{CL}}A$ into ${\Gamma }^N{⊢}_{\mathrm{IL}}{A}^N$. Induct on a natural deduction derivation. The translated logical conjunction, logical implication and universal rules are ordinary intuitionistic rules. Logical disjunction and existential introduction add double logical negation; their elimination rules first derive the double logical negation of the stable translated conclusion, then use its stability. Classical double-negation elimination translates precisely to stability. If logical equality atoms are double-negated, transport a stable translated conclusion through a logical equality by contradiction and then remove the resulting double logical negation. Original nonlogical axioms must also be translated; the result does not say arbitrary untranslated classical first-order theories are intuitionistically valid.

A first-order formula $A$ is stable when intuitionistic first-order logic proves $\neg \neg A\to A$. Double negations and logical falsity are stable. Logical conjunction of stable first-order formulas is stable; a logical implication is stable when its consequent is stable; and universal quantification preserves stability. For logical implication, from $\neg \neg (A\to B)$ and $A$, assuming $\neg B$ contradicts the first hypothesis, giving $\neg \neg B$ and then $B$. For universality, obtain $\neg \neg A(t)$ from $\neg \neg \forall xA(x)$ for arbitrary $t$, then use stability and generalize.

Classical first-order logic has the quantifier and logical equality rules of natural deduction together with unrestricted double-negation elimination, or equivalently the law of excluded middle. It is interpreted in ordinary two-valued first-order structures.

A first-order formula is built from atomic formulas using logical connectives and quantifiers over the elements of a structure.

The quantifier rank of a first-order formula is the maximum nesting depth of quantifiers. Atomic formulas have rank zero; negation preserves rank, binary Boolean connectives take the maximum, and either quantifier increases rank by one. It is not the total number of quantifiers.

Two first-order structures are rank-n equivalent if they agree on all sentences of quantifier rank at most $n$. The tuple version compares formulas at fixed tuples. For finite relational vocabulary this is equivalent to a Duplicator winning strategy in the $n$-round Ehrenfeucht-Fraïssé game.

A primitive positive formula is generated from atomic formulas using only logical conjunction and existential quantification. It can be put in the form $\exists \bar{y}{\bigwedge }_j{\theta }_j(\bar{x},\bar{y})$ with each ${\theta }_j$ atomic. The exam terminology tame formula refers to this fragment. Its reduced product transfer needs only filter intersection and upward closure, together with coordinatewise choices of witnesses.

Existential quantification forms $\exists x\phi (x,\mathbf{y})$. In a first-order structure, it is true at an assignment to $\mathbf{y}$ when some domain element makes the instance true. In natural deduction, elimination uses a fresh variable for the hypothetical witness; that variable may not escape into the conclusion or the remaining undischarged assumptions.

Universal quantification forms $\forall x\phi (x,\mathbf{y})$. In a first-order structure, it is true at an assignment to $\mathbf{y}$ when every domain element assigned to $x$ makes the instance true. Its introduction rule requires that the generalized variable not occur freely in undischarged assumptions.

A quantifier-free first-order formula is built from atomic formulas using logical connectives, with no quantifiers. An embedding of first-order structures preserves and reflects its truth, by mathematical induction on the first-order formula. Both positive and negated atomic information are needed for this conclusion in a relational language.

A quantifier-free sentence is a quantifier-free formula with no free variables. In a language whose only closed group terms denote zero, all quantifier-free sentences have the same truth value in every group, even when existential sentences distinguish them.

An atomic first-order formula is a relation applied to terms, or a logical equality of two terms when logical equality is included in the logic. It contains no logical connective or quantifier. Its truth is preserved and reflected by an embedding of first-order structures.

A first-order language specifies its constant, operation, and relation symbols, together with the arity of each nonconstant symbol.

A signature specifies the sorts, operation symbols with their input and output sorts, and relation symbols with their input sorts. The logical connectives and quantifiers are supplied separately by the chosen logic. This separates the nonlogical vocabulary from the rules defining a coherent theory.

For coding arithmetic computations, the signature in use is $0,1,+,\times ,<,=$. Bounded remainder tests and polynomial equations use only these symbols. This is a statement about the language: interpretation in the natural numbers does not impose the axioms of a ring.

A first-order term is built recursively from variables and constant symbols by applying function symbols to existing terms. Evaluation in a first-order structure follows the same recursion. An atomic formula applies a relation to terms, or asserts their logical equality.

A finite set of formulas mentions only finitely many nonlogical symbols. This observation lets compactness reduce arguments in a language indexed by a large set to a finite sublanguage.

An occurrence of a variable is free when it is outside the scope of a quantifier binding that variable.

A first-order sentence is a formula with no free variables, so its truth in a structure is independent of a variable assignment.

A first-order theory is a set of sentences in one first-order language. Depending on convention, the term may instead mean its deductive closure.

An arithmetic theory is sound if all its theorems hold in the standard natural numbers. Arithmetic soundness implies consistency and rules out a proof of the negation of a true sentence. It is a semantic property, distinct from effective axiomatizability.

Robinson arithmetic is a weak finitely axiomatized first-order theory sufficient for numeralwise representation of computable finite calculations and the Diagonal lemma. Its extensions are sufficiently strong for the soundness-based incompleteness argument.

A partial type over a first-order theory $T$ is a set of first-order formulas in a fixed finite tuple of variables which is jointly consistent with $T$. A tuple realizes it when it satisfies every formula in the set. A complete type additionally decides every formula in those variables.

For $A\subseteq M$, an A-type over first-order structure $M$ is a set of formulas in a fixed finite tuple of variables, with parameters in $A$, consistent with the complete theory of $M$ expanded by constants for $A$. Every finite subset is realized in $M$. A complete type decides all formulas in its variables over those parameters.

A partial type is nonprincipal when it is not a principal partial type. Equivalently, for every formula $\theta (\mathbf{x})$ consistent with $T$, some $\psi \in p$ makes $\theta \wedge \neg \psi$ consistent with $T$. This is the exact extension property needed in the Henkin construction proving the omitting types theorem.

A partial type $p(\mathbf{x})$ is principal over $T$ if some formula $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent implies each formula of $p$ modulo $T$. For complete types this is the usual notion of an isolated type. For an incomplete type, the isolating formula need not belong to the type itself.

A semidecidable axiomatization is a computably enumerable set of axioms. Its set of formal theorems is also computably enumerable by dovetailing over finite proofs.

The Craig trick converts an enumeration $A_1,A_2,\dots$ of axioms into a decidable equivalent set by replacing $A_i$ with a syntactically self-indexing repetition containing $i$ copies of $A_i$. A candidate of length $m$ can only encode one of the first $m$ axioms, so membership is decidable after computing that finite prefix.

In a conservative language extension, attach a fresh nullary predicate $P_i$ to the $i$th axiom $A_i$ and use a self-indexing copy of $P_i\wedge A_i$. The fresh tag makes each new axiom independent of all the others, while forgetting the tags recovers exactly the original-language consequences. The Craig trick makes the resulting axiom set decidable.

A Gödel numbering assigns natural numbers effectively to symbols, formulas, and finite proofs. Syntactic predicates such as “$p$ codes a proof in $T$ of the formula with code $q$” can then be represented by arithmetical formulas.

A natural number coding a finite syntactic object under a fixed Gödel numbering. For program descriptions it records a function in intension; different codes may denote the same function in extension.

For an effectively axiomatized arithmetic theory, a arithmetical provability predicate expresses that a formal proof of the sentence with a specified code exists. If axioms are only enumerated, proof certificates also record finite stages at which their axioms appear. The resulting predicate is arithmetically expressible.

For a finite list $(a_0,\dots ,a_{r-1})$ of nonnegative integers, encode its length with the exponent of two and its entries with the following prime numbers: $2^r{\prod }_{j<r}{p}_{j+2}^{a_j+1}$, where $p_i$ is the $i$th prime number. Unique prime factorization recovers both the length and entries. Requiring positive exponents on exactly the prescribed consecutive primes also makes validity decidable. Nesting list descriptors therefore gives a Gödel encoding of deterministic finite automata and other finite syntactic objects.

Peano arithmetic is the first-order theory of the natural numbers with zero, successor, addition, multiplication, order, and the induction scheme.

An internally finite subset of $\{0,\dots ,c-1\}$ can be represented in Peano arithmetic by a product of distinct prime numbers: multiply the $e$th prime number exactly when $e$ belongs to the subset. Divisibility by that prime recovers membership. Arithmetic induction proves existence of this code even for a definable subset with a nonstandard cutoff in a Nonstandard model of Peano arithmetic.

The theory of true arithmetic consists of all first-order arithmetic sentences true in the standard natural-number structure. It is complete but not computably enumerable.

Every nonempty definable set of natural numbers has a least element. Over the usual arithmetic language, this principle is equivalent to the induction scheme.

A nonstandard model of Peano arithmetic is a model not isomorphic to the standard natural-number structure. It contains the standard numerals as an initial segment and also contains elements larger than every standard numeral.

In a model of Peano arithmetic, an element realizes this partial type exactly when it is not a standard numeral. A model omitting it is isomorphic to the standard natural-number structure. For a complete consistent extension $T$ of arithmetic, the type is nonprincipal exactly when $T$ is the Theory of true arithmetic: apply the omitting types theorem in one direction and use an actual standard witness to refute any proposed isolating formula in the other. For incomplete theories, a principal partial type can still be omitted by some models.

The standard cut is the external initial segment consisting of the interpretations of the standard numerals. It is not definable, even with parameters, inside the nonstandard model.

If a definable property in a Nonstandard model of Peano arithmetic holds of every standard natural number, then it holds of some nonstandard element. Equivalently, a definable set containing the entire standard cut of a nonstandard model of arithmetic must overspill beyond it.

For every one-variable arithmetical formula $\theta (x)$, a sufficiently strong theory of arithmetic has a sentence $\gamma$ satisfying $\gamma \leftrightarrow \theta (┌\gamma ┐)$.

The Diagonal lemma can be carried out uniformly: from a one-variable formula code, compute a sentence code whose assertion is equivalent to the original formula applied to that sentence code. The effective substitution operation is what turns a semantic diagonal argument into a productive function.

Every consistent recursively axiomatized extension of elementary arithmetic is incomplete. If it were complete, its theorem set would be decidable; representing that decision procedure and diagonalizing against it yields a contradiction.

Tennenbaum's theorem says that no countable nonstandard model of Peano arithmetic can have both addition and multiplication computable under a presentation of its domain by the natural numbers.

Choose disjoint computably enumerable, recursively inseparable sets $A,B$. A nonstandard arithmetic model internally codes the elements enumerated into $A$ below a nonstandard stage by divisibility by standard primes. If the model's addition and multiplication were computable, division by each standard prime would decide the coded standard set. It would contain $A$ and avoid $B$, contradicting recursive inseparability.

A class of structures is first-order axiomatizable when it is exactly the class of models of some first-order theory. If extra constants are allowed, the corresponding class of reducts consists of structures that admit interpretations of those constants satisfying the theory.

The torsion-free groups are axiomatized by the group axioms together with, for every integer $n\ge 2$,

In the language with $\le$, total orders are axiomatized by reflexivity, antisymmetry, transitivity, and totality

A theory is consistent when it does not derive a contradiction. By first-order completeness, this is equivalent to having a model.

After fixing a Gödel numbering, the formal consistency statement $\mathrm{Con}(T)$ asserts that no natural number codes a $T$-proof of a contradiction. For a recursively axiomatized theory, this is an arithmetical sentence expressible inside any sufficiently strong base theory.

If $T$ is a consistent, recursively axiomatized theory containing enough arithmetic, then $T$ does not prove $\mathrm{Con}(T)$. The consistency assumption is external: an inconsistent theory proves every sentence, including its formal consistency statement.

For theories $T,S$ extending a fixed base theory, one consistency-strength comparison iswhere $C_T$ is the set of consequences of $T$ and $\mathrm{Cons}$ is the chosen class of formal consistency statements. Its strict part $T{<}_{\mathrm{Cons}}S$ means $T{\le }_{\mathrm{Cons}}S$ but not $S{\le }_{\mathrm{Cons}}T$.

Let $T=\mathrm{ZFC}+\text{“there is a worldly cardinal”}$ and $T^{\ast }=\mathrm{ZFC}+\mathrm{Con}(\mathrm{ZFC})$. A worldly $\kappa$ makes $V_{\kappa }$ a model of ZFC, and arithmetic absoluteness for a rank-initial model makes it a model of $T^{\ast }$, so $T$ proves $\mathrm{Con}(T^{\ast })$. If $T^{\ast }$ proved $\mathrm{Con}(T)$, then the stronger theory $T$ would prove its own consistency, contradicting the Gödel second incompleteness theorem. Thus, assuming consistency, $T^{\ast }{<}_{\mathrm{Cons}}T$.

Starting from a recursively axiomatized theory $T_0$, defineAssuming consistency, Gödel second incompleteness theorem makes every step strict in the consistency-strength preorder, while the effective union $T_{\omega }={\bigcup }_{n<\omega }{T}_n$ lies strictly above every finite stage.

Every theory containing an inconsistent subtheory is inconsistent, because the same finite derivation of contradiction remains available.

Every formal proof is a finite string and therefore uses only finitely many of the available assumptions.

A universal theory can be axiomatized by sentences whose quantifiers are all universal. Such sentences often forbid specified finite configurations.

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 first-order theory has its class of first-order models closed under substructures of a first-order structure exactly when it is equivalent to its universal consequences $T_{\forall }$. If $A\models T_{\forall }$, then $T\cup \mathrm{Diag}(A)$ is consistent. Otherwise a finite logical conjunction $\delta$ of signed diagram of a structure sentences yields a universal consequence $\forall \mathbf{x}\neg \delta (\mathbf{x})$ false in $A$. The compactness theorem gives a first-order model of $T$ containing an embedded copy of $A$, and closure under substructures of a first-order structure implies $A\models T$. The converse is preservation of universal sentences. The diagram of a structure must include negated as well as positive atomic sentences so that the resulting map is an embedding, not just a homomorphism.

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.

If failure of a property has a finite witness, one can often axiomatize the property by a universal sentence forbidding each possible finite witness. Compactness supplies finite witnesses when failure is expressed by inconsistency of an associated theory.

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

A structure embedding is an injective map respecting constants and operations and preserving and reflecting relations. Equivalently it preserves all atomic formulas and their negations. It identifies the source with a substructure of the target. An elementary embedding additionally preserves every first-order formula.

An $L$-substructure of a first-order structure $A\subseteq B$ has a nonempty domain containing all named constants and closed under the functions of $B$, and each relation of $A$ is the restriction of the corresponding relation of $B$. Consequently every quantifier-free formula with parameters in $A$ has the same truth value in $A$ and $B$. This is weaker than being an elementary substructure, which preserves all first-order formulas.

A substructure $M\subseteq N$ is simply closed when each existential quantifier-free formula over $M$ realized in $N$ is already realized in $M$. A single quantified variable suffices in the definition; iterating covers finite tuples. This property is also called existential closure in this specified extension. It is weaker than being an elementary substructure.

The satisfaction relation says that the finite code $e$ of a first-order formula is true in a set-sized first-order structure $A$ at assignment $\vec{a}$. It is defined uniformly in set theory by recursion on the finite syntax tree: evaluate atomic relations, Boolean operations and quantifiers over the given domain. A code includes only finitely many subformulas, and their truth relations are sets. This does not define a truth predicate for the ambient universe, whose domain is not a set. Finite relation closure for set-theoretic coding gives an explicit closure criterion ensuring that these truth relations are computed correctly in a transitive set.

A substructure $M\subseteq N$ is elementary when every first-order formula with parameters from $M$ has the same truth value in $M$ and $N$.

A substructure $M\subseteq N$ is elementary if and only if, whenever $N\models \exists x\phi (x,\bar{a})$ with parameters $\bar{a}$ from $M$, some witness $b\in M$ satisfies $N\models \phi (b,\bar{a})$.

After choosing a Skolem function for each existential formula, the Skolem hull of $A\subseteq N$ is the smallest subset containing $A$ and closed under those functions. The Tarski-Vaught test makes it an elementary substructure of $N$, and in a countable language an infinite hull has cardinality at most $|A|+{\aleph }_0$.

For each existential first-order formula $\exists y\phi (y,\mathbf{x})$ in a structure, a Skolem function selects a witness when one exists, with an arbitrary default when none exists. An expansion containing these functions satisfiesA subset closed under all such functions is elementary in the original language by the Tarski-Vaught test. Simultaneously choosing these functions is performed in the ordinary classical metatheory with choice.

A Skolem expansion adjoins a Skolem function for every existential first-order formula. Iterating through the successively enlarged languages, and taking their union, gives a language with witness functions even for first-order formulas involving previously added functions. Starting from a language of size $\kappa$, the resulting language has size at most $\kappa +{\aleph }_0$. A hull closed under its functions is a Skolem hull and is elementary in the expanded structure by the Tarski-Vaught test.