Formal Set-Theoretic Syntax, Structures, and Satisfaction

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

Terms and formulas as finite set codes defines every constructor by an explicit concatenation map $\mathrm{enc}$: outer parentheses and balance-one commas delimit token fields and complete child words. Terms and formulas are the least subsets of $W_L$ closed under those maps.

Let $P$ be a property of naturals such that for every $n\in \mathbb{N}$, if $P(m)$ holds for all $m<n$ then $P(n)$. Then $P(n)$ holds for all $n\in \mathbb{N}$. (At $n=0$ the hypothesis is vacuous, so $P(0)$ is forced.) (Strong (complete) induction)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

Every term and every formula in the delimited coding has exactly one outer constructor, with uniquely determined symbol fields and immediate subexpressions. Each immediate subexpression is shorter than its parent. (Unique parsing of finite syntax)

Let $(N,0,\sigma )$ be a Peano system (def-peano-system), in particular the natural numbers $\mathbb{N}$ (def-natural-numbers). For any set $A$, any element $a\in A$, and any function $f:A\to A$, there is a unique function $g:N\to A$ such that $g(0)=a$ and $g(\sigma (n))=f(g(n))$ for all $n\in N$. (The recursion theorem)

Let $P$ be a property of naturals such that for every $n\in \mathbb{N}$, if $P(m)$ holds for all $m<n$ then $P(n)$. Then $P(n)$ holds for all $n\in \mathbb{N}$. (At $n=0$ the hypothesis is vacuous, so $P(0)$ is forced.) (Strong (complete) induction)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

For an $L$-structure $\mathcal{M}$ and assignment $s\in M^{\omega }$, define $\mathrm{⟦}{v}_i{\mathrm{⟧}}_s=s(i)$, $\mathrm{⟦}c{\mathrm{⟧}}_s=c^{\mathcal{M}}$ and $\mathrm{⟦}f(t_1,\dots ,t_n){\mathrm{⟧}}_s=f^{\mathcal{M}}(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\mathrm{.}$ This is a simultaneous definition for all assignments: recurse on terms into the set $M^{(M^{\omega })}$ of functions from assignments to $M$. Variable leaves are projections, constant leaves are constant maps, and each function operation acts pointwise. Structural recursion gives a unique evaluation. The operations are total because the interpreted functions are total. Superscripts $\mathcal{M}$ on brackets will distinguish structures when needed. Conventions and prerequisites: def-set-structures-and-variable-assignments, thm-structural-recursion-on-set-coded-syntax. (Term denotation)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

For every set signature $L$ and $L$-structure $\mathcal{M}$ there is a unique set ${\mathrm{Sat}}_{\mathcal{M}}\subseteq {\mathrm{Form}}_L\times M^{\omega }$. Writing $\mathcal{M},s\models \varphi$ for membership, its clauses are $\mathcal{M},s\models u=v⟺\mathrm{⟦}u{\mathrm{⟧}}_s=\mathrm{⟦}v{\mathrm{⟧}}_s,$ $\mathcal{M},s\models R(t_1,\dots ,t_n)⟺(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\in R^{\mathcal{M}},$ $\mathcal{M},s\models \mathrm{\neg }\varphi ⟺\text{not }\mathcal{M},s\models \varphi ,$ $\mathcal{M},s\models \varphi \wedge \psi ⟺(\mathcal{M},s\models \varphi \text{ and }\mathcal{M},s\models \psi ),$ $\mathcal{M},s\models \mathrm{\exists }x\varphi ⟺\mathrm{\exists }b\in M(\mathcal{M},s[x:=b]\models \varphi )\mathrm{.}$ The set is uniformly first-order definable from $L$ and the structure data. (Existence and uniqueness of set satisfaction)

An occurrence is a token position in the parsed finite word. A variable occurrence is free when it is in a term field and no ancestor quantifier binds that variable. The variable field of a quantifier is a binder, not a free occurrence. Write $\mathrm{FV}(e)$ for the finite set of variables with free occurrences in $e$, and $\mathrm{Var}(e)$ for all variables appearing anywhere. A sentence is a formula with empty $\mathrm{FV}$. The recursive rules are $\mathrm{FV}(v)=\{v\}$, $\mathrm{FV}(c)=\mathrm{\varnothing }$, union over the arguments for function and atomic relation/equality expressions, unchanged under negation, union for conjunction, and $\mathrm{FV}(\mathrm{\exists }y\psi )=\mathrm{FV}(\psi )\setminus \{y\}$. Structural recursion justifies these set-valued definitions, with targets $\mathcal{P}(\omega )$ after identifying variables with their indices. Raw substitution $e[t\mathrm{/}x]$ replaces just the free occurrences of variable $x$ by term $t$. On terms it replaces $x$ by $t$, keeps other variables and constants, and acts on each argument. It commutes with atoms and Boolean constructors. At $\mathrm{\exists }y\psi$ it leaves the whole expression unchanged if $y=x$; otherwise it gives $\mathrm{\exists }y(\psi [t\mathrm{/}x])$. The term $t$ is free for $x$ in $e$ if, at every replaced occurrence, the path to the root crosses no binder for a member of $\mathrm{FV}(t)$. Thus at $\mathrm{\exists }y\psi$ with $y\mathrm{\ne }x$ and $x\in \mathrm{FV}(\psi )$ it requires both $y\mathrm{\notin }\mathrm{FV}(t)$ and that $t$ be free for $x$ in $\psi$. If no free $x$ occurs, the condition is vacuous. Simultaneous substitution replaces the original free occurrences once; it does not perform substitutions inside inserted terms. It need not equal sequential substitution. Conventions and prerequisites: thm-structural-recursion-on-set-coded-syntax. (Free variables and free-for substitution)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

For an $L$-structure $\mathcal{M}$ and assignment $s\in M^{\omega }$, define $\mathrm{⟦}{v}_i{\mathrm{⟧}}_s=s(i)$, $\mathrm{⟦}c{\mathrm{⟧}}_s=c^{\mathcal{M}}$ and $\mathrm{⟦}f(t_1,\dots ,t_n){\mathrm{⟧}}_s=f^{\mathcal{M}}(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\mathrm{.}$ This is a simultaneous definition for all assignments: recurse on terms into the set $M^{(M^{\omega })}$ of functions from assignments to $M$. Variable leaves are projections, constant leaves are constant maps, and each function operation acts pointwise. Structural recursion gives a unique evaluation. The operations are total because the interpreted functions are total. Superscripts $\mathcal{M}$ on brackets will distinguish structures when needed. Conventions and prerequisites: def-set-structures-and-variable-assignments, thm-structural-recursion-on-set-coded-syntax. (Term denotation)

An occurrence is a token position in the parsed finite word. A variable occurrence is free when it is in a term field and no ancestor quantifier binds that variable. The variable field of a quantifier is a binder, not a free occurrence. Write $\mathrm{FV}(e)$ for the finite set of variables with free occurrences in $e$, and $\mathrm{Var}(e)$ for all variables appearing anywhere. A sentence is a formula with empty $\mathrm{FV}$. The recursive rules are $\mathrm{FV}(v)=\{v\}$, $\mathrm{FV}(c)=\mathrm{\varnothing }$, union over the arguments for function and atomic relation/equality expressions, unchanged under negation, union for conjunction, and $\mathrm{FV}(\mathrm{\exists }y\psi )=\mathrm{FV}(\psi )\setminus \{y\}$. Structural recursion justifies these set-valued definitions, with targets $\mathcal{P}(\omega )$ after identifying variables with their indices. Raw substitution $e[t\mathrm{/}x]$ replaces just the free occurrences of variable $x$ by term $t$. On terms it replaces $x$ by $t$, keeps other variables and constants, and acts on each argument. It commutes with atoms and Boolean constructors. At $\mathrm{\exists }y\psi$ it leaves the whole expression unchanged if $y=x$; otherwise it gives $\mathrm{\exists }y(\psi [t\mathrm{/}x])$. The term $t$ is free for $x$ in $e$ if, at every replaced occurrence, the path to the root crosses no binder for a member of $\mathrm{FV}(t)$. Thus at $\mathrm{\exists }y\psi$ with $y\mathrm{\ne }x$ and $x\in \mathrm{FV}(\psi )$ it requires both $y\mathrm{\notin }\mathrm{FV}(t)$ and that $t$ be free for $x$ in $\psi$. If no free $x$ occurs, the condition is vacuous. Simultaneous substitution replaces the original free occurrences once; it does not perform substitutions inside inserted terms. It need not equal sequential substitution. Conventions and prerequisites: thm-structural-recursion-on-set-coded-syntax. (Free variables and free-for substitution)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

For any terms $u,t$, variable $x$, structure $\mathcal{M}$ and assignment $s$, put $b=\mathrm{⟦}t{\mathrm{⟧}}_s$. Then $\mathrm{⟦}u[t\mathrm{/}x]{\mathrm{⟧}}_s=\mathrm{⟦}u{\mathrm{⟧}}_{s[x:=b]}$. (Term substitution commutes with evaluation)

Assignments agreeing on $\mathrm{FV}(e)$ give equal denotations when $e$ is a term and the same truth value when $e$ is a formula. Also, passage to a reduct preserves denotations and satisfaction for expressions in the smaller signature. In particular sentence truth is independent of assignment; the truth of a formula can be specified by any tuple assigning all its free variables. (Coincidence for term values and satisfaction)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

If $t$ is free for $x$ in $\varphi$, then for every structure $\mathcal{M}$ and assignment $s$, $\mathcal{M},s\models \varphi [t\mathrm{/}x]⟺\mathcal{M},s[x:=\mathrm{⟦}t{\mathrm{⟧}}_s]\models \varphi \mathrm{.}$ (Free-for substitution commutes with satisfaction)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

If $z\mathrm{\ne }y$ is absent from $\mathrm{Var}(\psi )$, then $z$ is free for $y$ in $\psi$, and $\mathrm{\exists }y\psi$ and $\mathrm{\exists }z(\psi [z\mathrm{/}y])$ have the same truth in every structure and assignment. Here raw substitution replaces only occurrences free in $\psi$, hence only those bound by the displayed outer binder. A least fresh variable exists outside any specified finite set of variables. (Fresh bound-variable renaming preserves truth)

If $t$ is free for $x$ in $\psi$, then for every structure $\mathcal{M}$ and assignment $s$, $\mathcal{M},s\models \psi [t\mathrm{/}x]⟺\mathcal{M},s[x:=\mathrm{⟦}t{\mathrm{⟧}}_s]\models \psi \mathrm{.}$ (Free-for substitution commutes with satisfaction)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

There is a canonical total capture-avoiding substitution $\varphi ⟨t\mathrm{/}x⟩$ on formulas, obtained by renaming obstructing binders using least unused variable indices. It replaces the original free occurrences of $x$ and satisfies $\mathcal{M},s\models \varphi ⟨t\mathrm{/}x⟩⟺\mathcal{M},s[x:=\mathrm{⟦}t{\mathrm{⟧}}_s]\models \varphi \mathrm{.}$ Canonicity refers to the specified coding and traversal, not to literal invariance under other fresh-variable conventions. (Canonical capture-avoiding substitution)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

For every set signature $L$ and $L$-structure $\mathcal{M}$ there is a unique set ${\mathrm{Sat}}_{\mathcal{M}}\subseteq {\mathrm{Form}}_L\times M^{\omega }$. Writing $\mathcal{M},s\models \varphi$ for membership, its clauses are $\mathcal{M},s\models u=v⟺\mathrm{⟦}u{\mathrm{⟧}}_s=\mathrm{⟦}v{\mathrm{⟧}}_s,$ $\mathcal{M},s\models R(t_1,\dots ,t_n)⟺(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\in R^{\mathcal{M}},$ $\mathcal{M},s\models \mathrm{\neg }\varphi ⟺\text{not }\mathcal{M},s\models \varphi ,$ $\mathcal{M},s\models \varphi \wedge \psi ⟺(\mathcal{M},s\models \varphi \text{ and }\mathcal{M},s\models \psi ),$ $\mathcal{M},s\models \mathrm{\exists }x\varphi ⟺\mathrm{\exists }b\in M(\mathcal{M},s[x:=b]\models \varphi )\mathrm{.}$ The set is uniformly first-order definable from $L$ and the structure data. (Existence and uniqueness of set satisfaction)

An $L$-structure $\mathcal{M}$ has a nonempty set carrier $M$, values $c^{\mathcal{M}}\in M$, total functions $f^{\mathcal{M}}:M^{a(f)}\to M$, and relations $R^{\mathcal{M}}\subseteq M^{a(R)}$, supplied as set-indexed interpretation data. Logical equality is literal equality on $M$. An assignment is a function $s:\omega \to M$, also written $s(v_i)=s(i)$. The update $s[x:=b]$ changes only the value at variable $x$ to $b\in M$. For structures in the same signature a homomorphism $h:M\to N$ preserves constants and function values and takes related tuples to related tuples. It is strong if it also reflects every nonlogical relation. An embedding is an injective strong homomorphism; an isomorphism is a surjective embedding. A substructure has a nonempty subcarrier containing all constants, closed under all functions, with functions and relations restricted from the larger structure. A reduct keeps the carrier and only the interpretations for a smaller signature; an expansion is the reverse relationship. All finite powers and the assignment set $M^{\omega }$ are sets. Conventions and prerequisites: def-set-signature-and-finite-syntax-strings. (Structures and variable assignments)

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

Fix a pure membership formula $\delta (z,\vec{p})$ defining a class $C=\{z:\delta (z,\vec{p})\}$. This is eliminable notation for a predicate, not a class object. For a fixed pure membership formula $\varphi$, first rename its binders away from the parameter variables $\vec{p}$. Define ${\varphi }^C$ by keeping atoms, commuting with Boolean constructors, and setting $(\mathrm{\exists }x\psi {)}^C=\mathrm{\exists }x(\delta (x,\vec{p})\wedge {\psi }^C),(\mathrm{\forall }x\psi {)}^C=\mathrm{\forall }x(\delta (x,\vec{p})\to {\psi }^C)\mathrm{.}$ Copies of $\delta (x,\vec{p})$ are inserted by capture-avoiding substitution and fresh internal bound variables. In the set case $C=M$ use the predicate $z\in M$, with a fresh parameter variable for $M$. This operation is meaningful even for an empty class. It does not make the empty class an admitted structure: carriers of structures remain nonempty. For proper classes, evaluation of ${\varphi }^C$ means a separate ambient formula for each fixed $\varphi$, not a uniform universe satisfaction relation. Conventions and prerequisites: prop-capture-avoiding-substitution. (Relativization to sets and definable classes)

For every set signature $L$ and $L$-structure $\mathcal{M}$ there is a unique set ${\mathrm{Sat}}_{\mathcal{M}}\subseteq {\mathrm{Form}}_L\times M^{\omega }$. Writing $\mathcal{M},s\models \varphi$ for membership, its clauses are $\mathcal{M},s\models u=v⟺\mathrm{⟦}u{\mathrm{⟧}}_s=\mathrm{⟦}v{\mathrm{⟧}}_s,$ $\mathcal{M},s\models R(t_1,\dots ,t_n)⟺(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\in R^{\mathcal{M}},$ $\mathcal{M},s\models \mathrm{\neg }\varphi ⟺\text{not }\mathcal{M},s\models \varphi ,$ $\mathcal{M},s\models \varphi \wedge \psi ⟺(\mathcal{M},s\models \varphi \text{ and }\mathcal{M},s\models \psi ),$ $\mathcal{M},s\models \mathrm{\exists }x\varphi ⟺\mathrm{\exists }b\in M(\mathcal{M},s[x:=b]\models \varphi )\mathrm{.}$ The set is uniformly first-order definable from $L$ and the structure data. (Existence and uniqueness of set satisfaction)