Dependencies

Every consistent theory has a complete consistent extension.

If \(f(x)\) is a bounded formula in one free variable and \(t\) is a closed term, then one may form the sentence \(f(t)\) by substitution.

The colimit of a directed diagram is the quotient of the disjoint union of the stages by eventual equality.

A directed diagram is a family of objects indexed by a directed preorder, together with compatible transition maps along the preorder.

Given a predicate on the symbols of a language \(L\), the filtered language keeps exactly the symbols satisfying that predicate.

For each natural number \(n\), a bounded term or formula is a term or formula whose free variables lie among the first \(n\) variables.

For a set \(\Gamma \) of formulas, the relation \(\Gamma \vdash A\) is defined by a natural-deduction proof system with rules for assumptions, implication, universal quantification, falsity, equality, and substitution of equals.

A first-order language consists of function symbols and relation symbols, each sorted by arity.

The syntax carries two fundamental operations:

• lifting, which raises free variables above a chosen cutoff;

• substitution, which replaces a free variable by a term.

An \(L\)-structure consists of a carrier set together with interpretations of all function and relation symbols of \(L\).

The Henkin language chain starts from the original language at stage \(0\) and applies the one-step witness extension at each successor stage.

The Henkin language of a theory \(T\) is the limit language constructed from the language underlying \(T\).

The one-step Henkin extension of \(L\) is the language obtained by adjoining, for every bounded formula \(f(x)\), a new constant intended to witness \(f\).

Given a theory \(T\) over \(L\), the one-step Henkin extension is obtained by transporting \(T\) into the one-step Henkin language and adjoining all witness sentences for bounded one-variable formulas over \(L\).

For a formula \(f(x)\) and a constant \(c\), the witness property is the sentence

A homomorphism of first-order languages \(L \to L'\) is an arity-preserving map on function symbols together with an arity-preserving map on relation symbols.

Given a language map \(\varphi : L \to L'\) and an \(L'\)-structure \(M\), the reduct of \(M\) along \(\varphi \) is the \(L\)-structure obtained by restricting the interpretation to the image of \(L\).

For an injective language map with decidable image, reflection attempts to pull terms and formulas in the larger language back to the smaller language. Symbols outside the image are replaced by variables.

The infinite Henkin language \(L_\infty \) is the directed colimit of the finite Henkin language chain.

The theory \(T_\infty \) is the union, inside \(L_\infty \), of the images of all finite Henkin stages of the original theory.

Let \(c\) be a nonempty chain of consistent extensions of a theory \(T\). Every finite subset of the union of the chain is already contained in a single member of the chain.

The standard structure on \(\mathbb {Z}\) is a model of the chosen theory of abelian groups.

Each stage maps canonically into the colimit, and the colimit satisfies the expected universal property with respect to compatible families of maps out of the diagram.

The union of a chain of consistent extensions of \(T\) is again consistent.

Let \(T_1\) be a consistent theory. Suppose that every sentence \(\psi \) in a second theory \(T_2\) can be added to \(T_1\) without forcing inconsistency in the relevant one-step sense. Then the union \(T_1 \cup T_2\) is consistent.

If \(\Gamma \vdash A\), then every structure satisfying all formulas in \(\Gamma \) also satisfies \(A\).

The consistent limit theory obtained from the Henkin chain has enough constants.

If \(T_{\max }\) is maximal among the consistent extensions of a theory \(T\), then \(T_{\max }\) is complete.

A derivation in a language \(L\) can be transported along a language map \(L \to L'\) to a derivation in the larger language \(L'\).

Every consistent theory admits a complete Henkin extension in its Henkin language.

Suppose a constant symbol \(c\) does not occur in the assumptions \(\Gamma \) and does not occur in the formula \(f(x)\). If \(\Gamma \) proves the sentence \(f(c)\), then \(\Gamma \) proves \(\forall x\, f(x)\).

Every term, formula, bounded term, and bounded formula over \(L_\infty \) is represented by a unique compatible germ of corresponding syntax at a finite stage of the Henkin chain.

If \(T\) is consistent, then its one-step Henkin extension is also consistent.

If \(T\) is consistent, then every finite Henkin stage is consistent, the corresponding theories inside \(L_\infty \) are consistent, and the limit theory \(T_\infty \) is consistent.

Every consistent theory has a maximal consistent extension.

If a formula \(\psi \) is derivable from a set \(T\) of formulas, then there exists a finite subset \(\Gamma \subseteq T\) such that \(\Gamma \vdash \psi \).

If a sentence \(\psi \) is provable from a theory \(T\), then there is a finite subtheory \(\Gamma \subseteq T\) from which \(\psi \) is already provable.