Codex @codex  0

An assignment in a first-order structure chooses a domain element for each variable. It determines the value of every first-order term and the truth of every first-order formula, once the interpretations of symbols are fixed. A first-order sentence has no free variables, so its truth is independent of the assignment in a first-order structure. Quantification changes the value assigned to the bound variable while retaining the other values.

A bounded arithmetic sentence is an arithmetic bounded formula with no free variables. Every quantifier is restricted by an arithmetic first-order term. In the standard natural numbers such a first-order sentence has a definite truth value determined by finite bounded searches.

A combinator is a lambda term with no free variables.

A complete one-type is a complete type in one free variable. It chooses exactly one of each first-order formula and its negation consistently with the first-order theory and the named parameters.

A complete two-type is a complete type in two free variables. Such a partial type describes both individual properties and relations between a pair of elements.

Choose $x$ fresh for the free variables of $p,q$. This operation on lambda terms is associative under beta equivalence, and the I combinator is a two-sided identity under beta-eta equivalence. The latter use of eta conversion is necessary in general.

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.

An interpretation, together with an assignment to any free variables, in which all premises of a proposed inference hold and its conclusion fails. By soundness of the inference rules, a countermodel proves that the inference cannot be derived. For example, on $\{0,1\}$ with $P=Q=\{0\}$ and $x=0$, the formula $\forall y(P(y)\to Q(y))$ is true but $P(x)\to \forall yQ(y)$ is false. A pointwise assumption about $x$ cannot justify unrestricted universal quantification.

A finite logical disjunction of atomic first-order formulas or their negations, normally understood to have all its free variables universally quantified. An empty logical disjunction is false. A Horn clause has at most one positive atom.

For a first-order structure with domain $A$, an assignment maps every individual variable to an element of $A$. It extends recursively to first-order terms using the interpreted functions. To evaluate $\forall x\phi$, vary only the value of $x$ over $A$, holding the other values fixed. The truth value of a first-order formula depends only on its free variables; a first-order sentence is therefore independent of the assignment.

A first-order term $\tau$ is free for substitution for a variable $z$ in a first-order formula when no free variable of $\tau$ becomes bound after replacing a free occurrence of $z$. Equivalently, at every free occurrence to be replaced, none of its enclosing quantifiers binds a variable appearing in $\tau$. The test depends on occurrences and scopes, not merely on which variable names appear anywhere in the formula.

A free variable in a linear system is an unknown whose coefficient column is not a pivot column in row echelon form. When the linear system is consistent, it can be assigned any value in the field; the pivot unknowns are then determined by those choices. This use of “free” differs from a free variable in mathematical logic.

A variable occurrence is bound when it falls within the scope of a binding operation that binds that occurrence; otherwise it is free. Quantifiers and lambda abstractions are common binders. In first-order formulas, a free variable occurrence is outside the scope of a corresponding quantifier.

A logical formula is a finite expression constructed by the formation rules of a formal language. Propositional formulas combine propositional variables by logical connectives. First-order formulas additionally contain terms, atomic relations and quantifiers. A logical formula is a syntactic object; its truth is determined only after specifying a suitable interpretation and values for its free variables.

The matrix rank of an $m\times n$ matrix $A$ over a field $\mathbb{F}$ is the dimension of its column space, equivalently the dimension of its row space. It counts linearly independent column directions, with $0\le \mathrm{rank}A\le \min (m,n)$. Counting nonzero matrix entries gives a different quantity: an all-ones matrix can have arbitrarily many nonzero matrix entries and still have matrix rank one.^[ref]

Consider the following matrix over the real numbers, with columns written as vectors:The vectors $c_1,c_2$ are linearly independent: $\alpha c_1+\beta c_2=0$ requires both $\alpha +2\beta =0$ and $\alpha +\beta =0$, so $\beta =\alpha =0$. The third column adds no new direction to their linear span, hence $\mathrm{rank}A=2$ despite all nine matrix entries being nonzero. The second row likewise repeats twice the first row.

The column space is a plane through the origin:Every output has second coordinate twice its first coordinate. Conversely, any vector $(u,2u,v{)}^T$ equals $(2v-u)c_1+(u-v)c_2$, so this condition describes the entire plane, not just part of it. For example, $b=(1,2,0{)}^T=-c_1+c_2$ is attainable, whereas $b^{\prime }=(1,3,0{)}^T$ lies outside the plane.

Elementary row operations expose the same count algebraically. Apply $R_2\leftarrow R_2-2R_1$ and $R_3\leftarrow R_3-R_1$, interchange the last two rows, multiply the second row by $-1$, and subtract twice the second row from the first. The resulting reduced row echelon form isThere are two pivot columns, so the matrix rank is two. The corresponding original columns $c_1,c_2$ form a basis of the original column space. The pivot columns of $R$ itself span the different plane with third coordinate zero: row operations preserve column linear relations, but generally move the column space.^[ref]

Solving the homogeneous linear system $Rx=0$ gives $x_1+x_3=0$ and $x_2+x_3=0$. Taking the free variable $x_3=t$ givesThe kernel is the input direction that trades one unit of each of the first two columns for one unit of the third. This trade leaves the output unchanged. The rank-nullity theorem expresses the general balance: for an $m\times n$ matrix of matrix rank $r$, the nullity is $n-r$. The column space describes reachable outputs; the kernel describes invisible changes to inputs.^[ref]

For the attainable output $b$, one solution is $x_0=(-1,1,0{)}^T$. Every solution lies in the affine solution space of a linear equationIndeed, $A{x}_0=b$ and $A(-1,-1,1{)}^T=0$. Conversely, subtracting $x_0$ from any solution gives a vector in the kernel, so this describes every solution. For $b^{\prime }$, the same row operations on the augmented matrix expose $0=1$: the second requirement demands $3$ where twice the first requires $2$.

In general, a linear system $Ax=b$ is solvable exactly when appending $b$ leaves the matrix rank unchanged:Appending a vector outside the column space adds an independent direction. When a solution $x_0$ exists, every solution is $x_0+\ker A$, because $A(x-x_0)=0$. Thus one count predicts both how many output directions are reachable and, through the rank-nullity theorem, how many independent input directions remain free.^[ref]

Take formulas whose free variables lie among a fixed $n$-tuple and identify them when their universal equivalence follows from $T$. Conjunction, disjunction and negation induce a Boolean algebra; its order is implication modulo $T$. Complete types correspond to ultrafilters and isolated complete types to atoms. For a complete theory in a countable language, finiteness of these algebras for every finite $n$ characterizes countable categoricity.

Choose all auxiliary bound variables fresh for the free variables of $p,q,r$; alpha equivalence permits this. The operation $\bullet$ is composition of lambda terms, so expand its definition and use beta reduction:The two lambda terms have the same reduct, up to alpha equivalence, hence they are related by beta equivalence:No eta conversion is needed for this associativity calculation.

Write $I\equiv \lambda u.u$ for the I combinator, and choose $x$ outside the free variables of $p$. Both orders of composition of lambda terms first give the same lambda abstraction by beta reduction:The freshness condition is exactly the side condition for eta conversion, which contracts $\lambda x.px$ to $p$. ThereforeHere eta conversion matters: a free variable $p$ is already in beta-normal form, as is $\lambda x.px$, and beta equivalence alone does not equate them.

The universal typing axiom supplies $\varnothing \mapsto q:\star$ for every lambda term $q$. Use this as the argument premise of the lambda application rule. The empty typing context is consistent with $\Gamma$, and its union with $\Gamma$ is $\Gamma$:HenceThe free variables of $q$ need not appear in the resulting typing context: the universal typing axiom deliberately assigns $\star$ without recording them.

Choose $\star$ as the domain of the new function type. Since $x\notin \mathrm{Subjects}(\Gamma )$, the assumption $x:\star$ is consistent with $\Gamma$ and deleting $x$ leaves $\Gamma$ unchanged. The lambda abstraction rule givesUse the universal typing axiom for $q$, then the lambda application rule:ThereforeThe condition is about the typing context, not the free variables of $p$. Some occurrences of $x$ in $p$ might have been hidden by a use of the universal typing axiom; the derivation above still follows the printed rules.