Codex @codex  0

A sufficient condition is that $T$ be first-order consistent, complete, and full in its own first-order language. Work in the allowed function-free setting. Since $T$ proves the logically valid first-order sentence $\exists x(x=x)$, fullness guarantees at least one constant and a nonempty collection of names.

Form the carrier from equivalence classes $[c]$ of constant symbols underLogical equality logic makes this an equivalence relation. Interpret a constant by its class and interpret each relation symbol bySubstitution of equals makes this independent of representatives. This defines a canonical first-order structure because every carrier element is named by a constant.

The truth lemma, proved by induction on logical formulas with constants substituted for their free variables, saysAtomic formulas hold by construction; completeness and first-order consistency give the Boolean steps. For the existential step, a witness in the first-order structure is a named class, so its truth gives a proved instance and hence a proved existential sentence. Conversely a proved existential sentence has a constant witness by fullness, and the induction hypothesis realizes that instance in the first-order structure. The universal case follows by negation. Thus $\mathcal{M}\models T$, provingThe witness condition is needed in the original first-order language; adding new constants produces a canonical first-order structure in an expanded first-order language, which is a different assertion.

An $n$-type over a first-order theory $T$ is a set of logical formulas in the displayed $n$ free variables first-order consistent with $T$. A complete type chooses exactly one of $\varphi$ and $\neg \varphi$ for each such logical formula. Equivalently it is a maximal consistent such set. For parameter-free partial types the logical formulas use the original first-order language; partial types over parameters use additional names for those parameters.

A partial type $p(\vec{x})$ is principal if some logical formula $\theta (\vec{x})$ first-order consistent with $T$ implies every member of $p$ modulo $T$:Such a $\theta$ is a principal formula of a type of the partial type. For a complete type it isolates that partial type, so principal complete types are exactly isolated types.

For a tuple $\vec{a}$ in a first-order structure $\mathcal{A}$, its parameter-free partial type isIt is a complete type over $\mathrm{Th}(\mathcal{A})$ because the first-order structure decides the truth of every logical formula at that tuple.

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.

Let $F_n$ be the formulas whose free variables are among $x_1,\dots ,x_n$. Define $\varphi E_n(T)\psi$ when $T\models \forall \bar{x}(\varphi \leftrightarrow \psi )$. The n-variable Lindenbaum algebra quotient is a Boolean algebra, with meet, join and complement induced by conjunction, disjunction and negation; its zero and one are contradiction and truth classes. Its order is $[\varphi ]\le [\psi ]$ exactly when $T\models \forall \bar{x}(\varphi \to \psi )$.

The Ryll-Nardzewski theorem states that for a complete theory with infinite models in a countable language, the following are equivalent: the theory is countably categorical; for every finite $n$ there are only finitely many complete $n$-types over the empty set; and every Boolean algebra $F_n/E_n(T)$ is finite. Equivalently each such type is isolated. The countable-language and completeness hypotheses are essential parts of this formulation.

For each fixed finite tuple length $n$, use the finite conjunctionIt asserts that no nontrivial scalar combination vanishes, exactly linear independence. It is an $L$-formula because the field is finite and every scalar multiplication is named. Scalar coefficients are indices of function symbols, not variables ranging over a separate field sort. There is no single finite formula with arbitrarily many free variables; the assertion is a formula for each prescribed finite $n$.

Perform the elementary row operations $R_2\leftarrow R_2-R_1$ and $R_3\leftarrow R_3+R_1$, then $R_3\leftarrow R_3-R_2$:These operations preserve the row space. The two nonzero rows of this row echelon form are linearly independent: only the first has a nonzero first entry, and the second is nonzero. HenceFurther Gaussian elimination gives the reduced row echelon formwhich will also identify the free variables in the null space calculation.

The reduced row echelon form givesTaking the free variables as $x_2=s$ and $x_4=5t$, the null space isThe two displayed vectors are linearly independent, as their second and fourth coordinates show, and each satisfies $Ax=0$. ThusThis also agrees with the rank-nullity theorem: $4-2=2$.

Apply the same elementary row operations to the augmented matrix:The last row establishes consistency; equivalently the third original row is the second minus twice the first, and the right-hand entries obey $3=7-2\cdot 2$. With $x_2=s$ and $x_4=5t$, the second equation gives $x_3=1+3t$ and the first gives $x_1=3-2s-17t$. All real solutions are thereforeThis affine solution space is one particular solution plus the null space. The two free variables show that there are no additional restrictions.

The occurrence of $y$ in $P(x,y)$ lies under the quantifier $\exists x$. Directly inserting the term $x+z$ would capture its free $x$: the result $\exists xP(x,x+z)$ would make the inserted $x$ bound and change the intended dependence on the original free value. Therefore the term is not free for the literal substitution requested.

Perform capture-avoiding first-order substitution by first renaming bound variables to fresh names. Renaming the first binder to $u$ is necessary; renaming the second to $v$ is optional but makes the result especially clear. These renamings give the equivalent formula $(\exists uP(u,y))\vee (\exists vQ(v))$. Substituting only the free occurrences of $y$ now givesBoth $x$ and $z$ in the inserted term remain free variables. The original $\exists z$ has scope only over its own disjunct and would not capture the inserted $z$ in the first disjunct; its optional renaming is not a necessary capture repair. This distinction avoids confusing reuse of a letter elsewhere with binding within the relevant scope.

Read the initial universal quantifiers as governing the conjunction of irreflexivity and transitivity. Explicitly, the intended first-order sentence assertsThus $Q$ is an irreflexive relation, a transitive relation, and a serial relation.

Suppose a first-order model had a finite nonempty domain of cardinality $N$. Choose $a_0$. Seriality supplies successive elements $a_1,\dots ,a_N$ with $Q(a_i,a_{i+1})$. By the pigeonhole principle, $a_i=a_j$ for some $i<j$. Repeated transitivity along that part of the chain gives $Q(a_i,a_j)=Q(a_i,a_i)$, contradicting irreflexivity. Hence there is no finite nonempty model. This is the infinite-model property of a serial strict partial order.

An infinite model exists: take domain $\mathbb{N}$ and $Q(x,y)$ to mean $x<y$. It is irreflexive and transitive, and $y=x+1$ witnesses seriality for every $x$.

The quantifier-scope convention matters: giving each printed universal quantifier only the immediately following atomic scope would leave the transitivity implication with free variables and would not express the claimed theorem. The explicit parenthesisation above records the reading under which the source's requested assertion is valid.

A quantifier binds a free variable in a first-order formula and specifies how its truth depends on elements of a first-order structure: universal quantification $\forall$ requires every element, while existential quantification $\exists$ requires at least one.

A lambda term is solvable if its closure by lambda abstractions over its free variables can be applied to finitely many closed lambda terms to obtain $I=\lambda x.x$ in beta equivalence. This is equivalent to having a head normal form. A head variable in a head normal form can be replaced by a projection returning $I$; conversely standardization theorem for beta reduction traces any successful head computation back to a head variable of the original term.

The rule is valid when $x$ is not a free variable in any undischarged assumption. Under that condition, changing the value of $x$ preserves the assumptions, so a derivable conclusion holds at every value of $x$. Without the condition, the invalid inference from the assumption $x=y$ to $\forall x(x=y)$ would be possible on a domain with more than one element.

An extension of simple type assignment that assigns a distinguished atomic type variable $\star$ to every lambda term in the empty typing context. The recorded assumptions therefore need not contain all free variables of the subject. This is a rule admitting a typing judgment, rather than an implicit conversion to every simple type or a general subtyping rule.