Franklin's Notes


Adding definitions to models

When dealing with theories and models in first-order languages , translating statements of even relatively simple complexity quickly gets cumbersome. Normally, when we do mathematics, we introduce auxiliary notations and abbreviations so that we don't have to write out each logical statement in its entirety. I've already written up a list of some notational conventions , but as I start dealing with more complex models, it might be worth formalizing and streamlining the process of adding symbols to a language.

A model obtained by adding new functions, relations, and constants to an existing model is called an expansion , and the original model is called its reduct. The following principle justifies the introduction of new function and relation symbols which are already expressible in the original language:

Suppose $\mathfrak{A}$ is a model of the theory $\Sigma$ over a language $\mathscr{L}$.

Let $\mathscr{L}'=\mathscr{L}\cup{P}$, where $P$ is a new relation symbol, and suppose $\mathfrak{A}'$ is the expanded model of $\mathscr{L}'$ obtained by adding a relation $R$ to $\mathfrak{A}$ as the interpretation of $P$. Supppose $\varphi$ is a formula of $\mathscr{L}$ (so that it does not use the symbol $P$) with the property that $R(x_1...x_n)$ holds in $\mathfrak{A}'$ precisely when $\varphi[x_1...x_n]$ holds. Then each sentence of $\mathscr{L}$ holds in $\mathfrak{A}$ iff it holds in $\mathscr{L}'$. Additionally, if $T'$ is the theory obtained by adding the axiom $P(v_1...v_n)\leftrightarrow \varphi(v_1...v_n)$ to $T$ (which can be viewed as a "definition" of the symbol $P$), then each sentence of $\mathscr{L}$ is provable from/consistent with $T$ if and only if it is provable from/consistent with $T'$.

Now, suppose $\mathscr{L}'=\mathscr{L}\cup{F}$, where $F$ is a new function symbol, and suppose $\mathfrak{A}'$ is the expanded model of $\mathscr{L}'$ obtained by adding a function $G$ to $\mathfrak{A}$ as the interpretation of $F$. Suppose $\varphi$ is a formula of $\mathscr{L}$ (not using the symbol $F$) with the property that $G(x_1...x_m)=y$ holds in $\mathfrak{A}'$ precisely when $\varphi[x_1...x_my]$ holds. Then each sentence of $\mathscr{L}$ holds in $\mathfrak{A}$ iff it holds in $\mathscr{L}'$. Additionally, if $T'$ is the theory obtained by adding the axiom to $T$, then each sentence of $\mathscr{L}$ is provable from/consistent with $T$ if and only if it is provable from/consistent with $T'$, so long as the sentence is provable from/consistent with $T$ as well.

Why is this true? Well, if a relation $R(x_1...x_n)$ holds whenever some statement $\varphi[x_1...x_n]$ from the reduced language is satisfied, and $\psi$ is some sentence involving $P$, we may simply replace each occurrence of $P(v_1...v_n)$ in $\psi$ with the string $\varphi(v_1...v_n)$, so long as we take care to rename variables appropriately to avoid repeats.

Similarly with new functions, but we must be a bit more careful in this case, for defining a function implicitly in terms of a formula $\varphi$ presupposes some information about $\varphi$ - namely, that it uniquely defines the value of that function for all inputs. Suppose, for instance, that we were working with a theory of some field, and we attempted to define a new function with the following axiom: This would be an attempt at defining a "square root" function on a field. However, not all theories of fields are consistent with the existence of unique square roots - consider for example $\mathbb Q$, where some numbers have no square root and others have two. On the other hand, some field theories may be consistent with the existence of square roots without entailing them, whereby the above axiom would inadvertently "add information" to the original theory (by implying that square roots are uniquely defined).

So long as we are careful, we can add new symbols to languages without affecting which statements are provable/consistent in the original language, or which statements are true in particular models.

model-theory

first-order-logic

back to home page